proposition: Lemma ge_le_iff p q : p >= q <-> q <= p.
proof: Proof. unfold le, ge. now rewrite compare_antisym, CompOpp_iff. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef