proposition: Lemma geb_leb n m : (n >=? m) = (m <=? n).
proof: Proof. unfold geb, leb. rewrite compare_antisym. now case compare. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass