rw [mul_self_pos, sub_ne_zero]
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
⊢ 0 < (x - y) * (x - 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
⊢ x ≠ y