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