Ssreflect Users Discussion List

[Michael Shulman <>]

Hello,

In the homotopy type theory Coq library we have started using some of
the basic definitions and proofs about natural numbers inspired by
SSR.  However there is one thing I am puzzled by: why is "n < m" a
Notation for "S n <= m" rather than a Definition?  I appreciate the
advantage of having the two be judgmentally equal, but it's not
obvious to me why one would want them to be syntactically equal (i.e.
without having to unfold a definition).  Moreover, I find it confusing
to have hypotheses of the form "S n <= m" automatically transformed
into "n < m" (e.g. in the inductive step of an induction on n with a
previous hypothesis of "n <= m"); the two are not syntactically equal
in my head.  Can someone explain?

Thanks!
Mike