proposition: Lemma nat_ne_0_pos x : x ≠ 0 ↔ 0 < x.
proof: Proof. split. destruct (nat_0_or_pos x); intuition. intros E1 E2. rewrite E2 in E1. now destruct (irreflexivity (<) 0). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings MathClasses.orders.nat_int