【Lean4】induction

induction

自然数や帰納的に定義された対象について帰納法を使う

Plaintext

example (n : ℕ) : n + 0 = n := by
  induction n with
  | zero =>
      rfl
  | succ n ih =>
      simp [ih]

/-
自然数の場合、
zeroの場合
succ nの場合
に分かれる
-/

example (n : ℕ) : n + 0 = n := by
  induction n with
  | zero =>
      rfl
  | succ n ih =>
      simp [ih]

/-
自然数の場合、
zeroの場合
succ nの場合
に分かれる
-/