## Stream: Coq users

### Topic: n <= m

#### Rafael Garcia Leiva (Aug 05 2020 at 16:13):

Hi,

Still learning Coq. Can somebody help me to prove the following Lemma?

Lemma equivalence (n m : nat):
n <= m <-> (n < m \/ n = m).

#### Daniel Sousa (Aug 05 2020 at 16:50):

Sure! What progress have you been able to do so far? Where are you stuck?

#### Rafael Garcia Leiva (Aug 05 2020 at 18:30):

Hi,

I have checked the standard library with:

SearchPattern (nat -> nat -> bool).
Search Nat.leb.

and

Locate "_ <= _".
Search Nat.le.

but it seems this property is not included.

Also, I have tried:

Proof.
split.
intros.
firstorder.

and

Proof.
split.
intros.
left.
auto.

Many thanks!

#### Yishuai Li (Aug 05 2020 at 20:26):

Have you tried using evidence in proofs?

#### Yishuai Li (Aug 05 2020 at 20:29):

More specifically, induction on evidence.

#### Rafael Garcia Leiva (Aug 06 2020 at 08:01):

Hi,

I have managed to prove it with:

Lemma equivalence (n m : nat):
n <= m <-> (n < m \/ n = m).
Proof.
split.
intros.
induction H.
right.
reflexivity.
left.
assert (m < S m).
auto.
firstorder.
intros.
destruct H as [H1 | H2].
induction H1.
auto.
auto.
induction H2.
auto.
Qed.

But probably there is an easier way :)

Side note: in the Mathematical Components library we found that a different definition of `leq` works better. In particular one can define `leq` as a program rather than as a (functional) relation. See https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssrnat.html for the file about arithmetic (search for `Definition leq`) and here you can find a more extensive doc about this formalization style: https://math-comp.github.io/mcb/