proposition: Lemma gt_lt_iff n m : n > m <-> m < n.
proof: Proof. unfold lt, gt. now rewrite compare_antisym, CompOpp_iff. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass