`{FullPseudoSemiRingOrder N} `{!NaturalsToSemiRing N} `{!Naturals N} `{FullPseudoSemiRingOrder R} `{!IsSemiCRing R} `{!IsSemiRingPreserving (f : N -> R)} n : 0 ≤ f n. Proof. revert n. apply naturals.induction. - rewrite (preserves_0 (f:=f)). reflexivity. - intros n E. rewrite (preserves_plus (f:=f)), (preserves_1 (f:=f)). apply nonneg_plus_compat. + solve_propholds. + trivial. Qed.
Require Import