## Stream: math-comp users

### Topic: n.+1 vs (n + 1)

#### Julin Shaji (Feb 21 2024 at 18:12):

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.
``````

`(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.

#### Julin Shaji (Feb 21 2024 at 18:17):

Oh, I just needed `ltP`:

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

#### Julin Shaji (Feb 21 2024 at 18:23):

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
*)
``````

#### Julin Shaji (Feb 21 2024 at 18:24):

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.
``````

#### Cyril Cohen (Feb 22 2024 at 08:04):

``````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.

#### Cyril Cohen (Feb 22 2024 at 08:07):

``````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.

#### Ana de Almeida Borges (Feb 22 2024 at 14:19):

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.
``````

`(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`.

#### Julin Shaji (Feb 22 2024 at 16:59):

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