proposition: Theorem leb_le p q : (p <=? q) = true <-> p <= q.
proof: Proof. unfold leb, le. destruct compare; easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef