x y : x < y <-> exists z, y = x + 1 + naturals_to_semiring N R z. Proof. split. - intros E. destruct ((fst (nat_int_le_plus x y) (lt_le _ _ E))) as [z0 Ez]. destruct (naturals.case z0) as [E1|[z E1]];rewrite E1 in *;clear z0 E1. + rewrite preserves_0, plus_0_r in Ez. destruct (lt_ne_flip x y);trivial. + exists z. rewrite (preserves_plus (A:=N)), preserves_1, plus_assoc in Ez. trivial. - intros [z Ez]. rewrite Ez. apply nonneg_plus_lt_compat_r. + apply to_semiring_nonneg. + apply pos_plus_lt_compat_r; solve_propholds. Qed.
Require Import