proposition: Lemma compare_le_iff p q : (p ?= q) <> Gt <-> p <= q.
proof: Proof. reflexivity. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef