proposition: Lemma nat_int_lt_plus x y : x < y ↔ ∃ z, y = x + 1 + naturals_to_semiring nat R z.
proof: Proof. split. intros E. destruct (proj1 (nat_int_le_plus x y)) as [[|z] Ez]. now apply lt_le. rewrite O_nat_0, preserves_0, plus_0_r in Ez. now destruct (lt_ne_flip x y). exists z. now rewrite S_nat_1_plus, preserves_plus, preserves_1, associativity in Ez. intros [z Ez]. rewrite Ez. apply nonneg_plus_lt_compat_r. now apply to_semiring_nonneg. apply pos_plus_lt_compat_r; solve_propholds. 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