Library Coq.Arith.Compare_dec
Proofs of decidability
A ternary comparison function in the spirit of Z.compare.
See now Nat.compare and its properties.
In scope nat_scope, the notation for Nat.compare is "?="
Some projections of the above equivalences.
A previous definition of nat_compare in terms of lt_eq_lt_dec.
The new version avoids the creation of proof parts.
A boolean version of le over nat.
See now Nat.leb and its properties.
In scope nat_scope, the notation for Nat.leb is "<=?"