ring_nf at this ⊢
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * (2 * z * z + 2 * z + 1) ≤ 2 * (x * x + y * y)
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
⊢ 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2