The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 24/06/2020 à 07:30, Gabriel Scherer a écrit :

> On the other hand, you could define a "smaller" type of inequivalence
> for a type (as an inductive presentation if you can, for example) that
> has better properties. This comes up often in cases where you need to
> reason on elements being equal, as the definition of inequivalence as a
> function makes it hard to reason about.
> For natural numbers for example, one definition of inequivalence might
> be something like
> 
> Inductive different :=
> | Bigger : forall (k : nat), m = n + S k -> different m n
> | Smaller : forall (k : nat), m + S k = n -> different m n.

If one is going the way of representing disequalities by equalities to
ensure uniqueness of proofs, then the boolean encoding seems a bit simpler:

Definition different m n := Nat.eqb m n = false.

Best regards,

Guillaume