Doubling distributes over addition

Theorem · two_mul_add

Doubling distributes over addition: $2(a + b) = 2a + 2b$ .

Formal statement · Lean 4.lean

theorem two_mul_add (a b : Nat) : 2 * (a + b) = 2 * a + 2 * b := by
  sorry

Proof. sorry

Nobody has tried yet.