proposition: Lemma to_semiring_nonneg `{FullPseudoSemiRingOrder N} `{!NaturalsToSemiRing N} `{!Naturals N} `{FullPseudoSemiRingOrder R} `{!IsSemiRing R} `{!IsSemiRingPreserving (f : N -> R)} n : 0 ≤ f n.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.naturals HoTT.Classes.theory.rings HoTT.Classes.orders.semirings