proposition: Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).
proof: Proof. rewrite geb_leb. apply leb_spec. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass