proposition: Lemma nat_not_neg x : ¬x < 0.
proof: Proof. apply le_not_lt_flip, nat_nonneg. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings MathClasses.orders.nat_int