x : 0 ≤ x -> exists z, x = naturals_to_semiring N R z. 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.
Require Import