proposition: Lemma induction : forall (P: N -> Type), P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n.
proof: Proof. pose (Q := fun s : SemiRings.Operations => forall P : s -> Type, P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n). change (Q (SemiRings.BuildOperations N)). apply (from_nat_stmt nat). unfold Q;clear Q. simpl. exact nat_induction. Qed.
imports: HoTT.Basics.Decidable HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.theory.rings HoTT.Classes.isomorphisms.rings HoTT.Classes.interfaces.naturals