Ssreflect Users Discussion List

[Vincent Siles <>]

More precisely, ssrnat and coqnat are the exact same type, but
the lt function is different. ssr function is a decidable function
nat -> nat -> bool whereas coq's function is nat -> nat -> Prop.

The lemma ltP is the one that links both functions.

Cheers,
Vincent

2011/6/8 Reynald Affeldt <>:
>
>> Require Import ssrbool ssrnat.
>> Lemma nat_conv : forall (n m: nat),
>>  (n < m)%nat  -> (n < m)%coq_nat.
>
> by move=>*; apply/ltP.
>
> does it
>
>