Theorem Marketplace

Theorem Details

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

Bounty: 0.0008 ETH

Status: Closed

Proof

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

Back to Bounties