proposition: Lemma nat_int_to_semiring x : ∃ z, x = naturals_to_semiring nat R z ∨ x + naturals_to_semiring nat R z = 0.
proof: Proof. revert x. apply biinduction. solve_proper. exists 0. left. now rewrite preserves_0. intros n; split. intros [z [Ez | Ez]]. exists (1 + z). left. now rewrite preserves_plus, preserves_1, Ez. destruct z as [|z]. exists 1. left. rewrite O_nat_0, preserves_0, plus_0_r in Ez. rewrite Ez, preserves_1. ring. exists z. right. rewrite S_nat_1_plus, preserves_plus, preserves_1 in Ez. rewrite <-Ez. ring. intros [z [Ez | Ez]]. destruct z as [|z]. exists 1. right. rewrite O_nat_0, preserves_0 in Ez. rewrite preserves_1, <-Ez. ring. exists z. left. rewrite S_nat_1_plus, preserves_plus, preserves_1 in Ez. now apply (left_cancellation (+) 1). exists (1 + z). right. rewrite preserves_plus, preserves_1, <-Ez. ring. 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