Ssreflect Users Discussion List

[Marcus Ramos <>]

Hi,

In library "ssrnat" I find the definition:

Lemma addn_eq0 : forall m n, (m + n == 0) = (m == 0) && (n == 0).

I can´t, however, figure out the difference between "==" and "=", nor find "==" in the Coq documents. Is this something specific to SSReflect?

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

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

Thanks in advance,

Marcus.