Ssreflect Users Discussion List

[Guillaume Cano <>]

Hi,

Is there an equivalent "forall m n: nat, (m + n) = 0 -> (m = 0) /\ (n = 0)" anywhere?

It is addn_eq0.

I also couldn´t find a (nat) lemma like "forall n: nat, (n = 0) -> n <= 0". Does it exist anywhere?

You are also lemmas eq_leq or leqn0 in ssrnat.v

Since nat has eqType structure, many lemmas are expressed as equality between booleans rather than 

equivalence between propositions.

Best,

Guillaume.