proposition: Lemma nat_induction (P : nat → Prop) : P 0 → (∀ n, P n → P (1 + n)) → ∀ n, P n.
proof: Proof. Proof nat_ind P. #[global] Instance: Initial (semirings.object nat). Proof. intros. apply natural_initial. intros. intros x y E. unfold equiv, nat_equiv in E. subst y. induction x. replace 0%nat with (zero:nat) by reflexivity. rewrite 2!rings.preserves_0. reflexivity. rewrite S_nat_1_plus. rewrite 2!rings.preserves_plus, 2!rings.preserves_1. now rewrite IHx. Qed.
imports: Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base Coq.Arith.PeanoNat MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings