Proofs

Proof by induction

Prove a property for all natural numbers using a base case and a successor case.

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp only [Nat.add_succ, ih]

#check zero_add

Explanation

Splits a proof into zero and successor cases, following Nat’s constructors.

The induction hypothesis: the property is already known for the smaller n.

Simplifies using the listed lemmas and built-in reductions, without the default simp lemma set.

Reference only. Run the file to check its actual result.

zero_add (n : Nat) : 0 + n = n

Inspect the successor case and explain where the induction hypothesis is used.