Library Coq.Num.GeAxioms


Require Export Axioms.

Require Export LtProps.

Axiomatizing >= from <





Axiom not_lt_ge : (x,y:N)~(x<y)->(x>=y).

Axiom ge_not_lt : (x,y:N)(x>=y)->~(x<y).




Hints Resolve not_lt_ge : num.

Hints Immediate ge_not_lt : num.