proposition: Lemma nat_0_or_pos x : x = 0 ∨ 0 < x.
proof: Proof. destruct (trichotomy (<) 0 x) as [?|[?|?]]; intuition. now destruct (nat_not_neg x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings MathClasses.orders.nat_int