induction0.lean

import Mathlib.Tactic

open Nat

theorem induction0 {P : ℕ → Prop}
  (base : P 0) (step : ∀m, P m → P (succ m)) : (∀n, P n) := by
    intro k
    cases k with
    | zero => exact base
    | succ m =>
        apply step
        apply induction0 /- is this recursion valid? -/
        exact base
        exact step
    done