proposition: Lemma induction (P: N → Prop) `{!Proper ((=) ==> iff) P}: P 0 → (∀ n, P n → P (1 + n)) → ∀ n, P n.
proof: Proof. intros. rewrite <-(to_semiring_involutive _ nat n). generalize (naturals_to_semiring N nat n). clear n. apply nat_induction. now rewrite preserves_0. intros n. rewrite preserves_plus, preserves_1. auto. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings Coq.Arith.PeanoNat MathClasses.categories.varieties MathClasses.theory.ua_transference MathClasses.interfaces.naturals