proposition: Lemma geb_ge n m : (n >=? m) = true <-> n >= m.
proof: Proof. unfold geb, ge. destruct compare; easy'. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass