rw [h]
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (x + y) * (x + y) = 4 * z * z + 4 * z + 1
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (2 * z + 1) * (2 * z + 1) = 4 * z * z + 4 * z + 1