proposition: Lemma nat_int_le_plus x y : x ≤ y <-> exists z, y = x + naturals_to_semiring N 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. rewrite <-Eu. trivial. - intros [z Ez]. rewrite Ez. apply nonneg_plus_le_compat_r, to_semiring_nonneg. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.naturals HoTT.Classes.theory.rings HoTT.Classes.orders.semirings