proposition: Lemma nat_int_nonneg_decompose x : 0 ≤ x -> exists z, x = naturals_to_semiring N R z.
proof: Proof. destruct (nat_int_to_semiring x) as [z [Ez1 | Ez2]]. - exists z. trivial. - intros E. exists 0. rewrite (preserves_0 (A:=N)). apply (antisymmetry (≤)); trivial. rewrite <-Ez2. apply nonneg_plus_le_compat_r. apply 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