proposition: Lemma nat_int_nonneg_decompose x : 0 ≤ x → ∃ z, x = naturals_to_semiring nat R z.
proof: Proof. destruct (nat_int_to_semiring x) as [z [Ez1 | Ez2]]. now exists z. intros E. exists 0. rewrite preserves_0. apply (antisymmetry (≤)); auto. rewrite <-Ez2. now apply nonneg_plus_le_compat_r, to_semiring_nonneg. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals MathClasses.orders.semirings