Theorem Marketplace

Theorem Details

-- commutativity of addition

theorem add_comm (a b : Nat) : a + b = b + a := by sorry

Bounty: 0.05 ETH

Status: Closed

Proof

-- commutativity of addition --

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero =>
    rw [Nat.add_zero, Nat.zero_add]
  | succ b ih =>
    rw [Nat.add_succ, ih, Nat.succ_add]

Back to Bounties