forall x : R, exists z, x = naturals_to_semiring N R z |_| (x + naturals_to_semiring N R z)%mc = 0. Proof. apply biinduction. - exists 0. left. symmetry. apply preserves_0. - intros. split;intros E. + destruct E as [z [E|E]]. * exists (1+z). left. rewrite E. rewrite (preserves_plus (f:=naturals_to_semiring N R)), (preserves_1 (f:=naturals_to_semiring N R)). reflexivity. * destruct (naturals.case z) as [Ez|[z' Ez]]. ** rewrite Ez in *. rewrite (preserves_0 (A:=N)),plus_0_r in E. rewrite E. exists 1. left. rewrite (preserves_1 (A:=N)),plus_0_r. reflexivity. ** rewrite Ez in *;clear z Ez. exists z';right. path_via (n + naturals_to_semiring N R (1 + z')). clear E. rewrite (preserves_plus (A:=N)),(preserves_1 (A:=N)). rewrite plus_assoc,(plus_comm n);reflexivity. + destruct E as [z [E|E]]. * destruct (naturals.case z) as [Ez|[z' Ez]];rewrite Ez in *;clear z Ez. ** exists 1;right. rewrite (preserves_1 (A:=N)),plus_comm,E. apply preserves_0. ** exists z';left. rewrite (preserves_plus (A:=N)),(preserves_1 (A:=N)) in E. apply (left_cancellation plus 1). trivial. * exists (1+z). right. rewrite (preserves_plus (A:=N)), (preserves_1 (A:=N)),<-E. rewrite plus_assoc,(plus_comm n);reflexivity. Qed.
Require Import