proposition: Lemma to_semiring_nonneg `{FullPseudoSemiRingOrder N} `{!NaturalsToSemiRing N} `{!Naturals N} `{FullPseudoSemiRingOrder R} `{!SemiRing_Morphism (f : N → R)} n : 0 ≤ f n.
proof: Proof. pose proof (pseudo_srorder_semiring (A:=R)). revert n. apply naturals.induction. solve_proper. intros. now rewrite preserves_0. intros n E. rewrite preserves_plus, preserves_1. apply nonneg_plus_compat. solve_propholds. easy. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals MathClasses.orders.semirings