rw [← add_sq_add_sq_sub, h', add_le_add_iff_left]
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 1 ≤ (x - y) * (x - y)