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