I was trying to prove this goal:

```
From mathcomp Require Import all_ssreflect.
Require Import Arith.
Goal forall n m:nat,
n.+1 < m.+1 -> n < m.
Proof.
move => n m H.
Check (ltn_add2r 1) n m.
```

`(ltn_add2r 1) n m`

would give `(n + 1 < m + 1) = (n < m)`

but I couldn't figure how to use it.

I guess it's because mathcomp uses `addn`

and coq stdlib uses `Nat.add`

?

How can we get around this?

I tried unfolding with `rewrite /addn`

, but that changed nothing.

Oh, I just needed `ltP`

:

```
Goal forall n m:nat,
n.+1 < m.+1 -> n < m.
Proof.
move => n m /ltP //=.
Qed.
```

But how could this be solved though?

```
Goal forall (n m: nat),
(forall a b:nat, a < b) -> n.+1 < m.+1.
Proof.
move => n m IH.
(*
1 subgoal
n, m : nat
IH : forall a b : nat, a < b
========================= (1 / 1)
n.+1 < m.+1
*)
```

I guess this is a way:

```
Goal forall (n m: nat),
(forall a b:nat, a < b) -> n.+1 < m.+1.
Proof.
move => n m H.
have HH := H n m.
move: HH.
by move /ltP.
Qed.
```

```
From mathcomp Require Import all_ssreflect.
Goal forall n m : nat, n.+1 < m.+1 -> n < m.
Proof. by []. Qed.
```

The reason is `.+1`

is a notation for constructor `S`

and the definition of `<`

(or in fact `<=`

) reduces partially.

```
From mathcomp Require Import all_ssreflect.
Goal forall (n m : nat), (forall a b : nat, a < b) -> n.+1 < m.+1.
Proof. by move=> n m ->. Qed.
```

because the conclusion of the third hypothesis is in fact `(?a < ?b) = true`

and the left hand side matches the goal.

Julin Shaji said:

I was trying to prove this goal:

`From mathcomp Require Import all_ssreflect. Require Import Arith. Goal forall n m:nat, n.+1 < m.+1 -> n < m. Proof. move => n m H. Check (ltn_add2r 1) n m.`

`(ltn_add2r 1) n m`

would give`(n + 1 < m + 1) = (n < m)`

but I couldn't figure how to use it.I guess it's because mathcomp uses

`addn`

and coq stdlib uses`Nat.add`

?How can we get around this?

I tried unfolding with

`rewrite /addn`

, but that changed nothing.

Do you mean to be mixing mathcomp `nat`

and stdlib `nat`

? Typically once one has the former there is no need to import `Arith`

.

I had a few lemmas which were made without mathcomp. I wanted to use them in a proof where mathcomp is also imported.

Last updated: Jul 15 2024 at 21:02 UTC