proposition: Lemma nat_int_le_plus x y : x ≤ y ↔ ∃ z, y = x + naturals_to_semiring nat R z.
proof: Proof. split. intros E. destruct (decompose_le E) as [z [Ez1 Ez2]]. destruct (nat_int_nonneg_decompose _ Ez1) as [u Eu]. exists u. now rewrite <-Eu. intros [z Ez]. rewrite Ez. 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