Ssreflect Users Discussion List

[Laurent Théry <>]

On 04/15/2014 03:30 PM, Marcus Ramos wrote:

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?
Yep  == represents the equality of an eqtype,  = the propositional equality

Check (1 = 2).
1 = 2
     : Prop

Check (1 == 2).
1 == 2
     : bool

The relation between the two is part of the reflection of 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?

These lemmas could easily be simulated with that is present in the library (for example the first one is
just the reflected verion of your first theorem)