proposition: Lemma le_refl p : p <= p.
proof: Proof. intros. unfold le. now rewrite compare_refl. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef