Theorem: Turanpartition.square (Turan4/Turanpartition.lean)

State before:
b c : ℕ
⊢ (b + c) ^ 2 = b ^ 2 + 2 * b * c + c ^ 2
Tactic:
rw [pow_two,add_mul, mul_add,mul_add,pow_two,pow_two,mul_comm c,two_mul,add_mul,add_assoc,add_assoc,add_assoc]
State after:
no goals