2D Euclidean Midpoint Sphere Strict Convexity

import Mathlib

theorem euclidean_2d_sphere_midpoint_strict (x z : ℝ × ℝ) (R : ℝ) (hx : x.1 ^ 2 + x.2 ^ 2 = R) (hz : z.1 ^ 2 + z.2 ^ 2 = R) (h_mid : ((x.1 + z.1) / 2) ^ 2 + ((x.2 + z.2) / 2) ^ 2 = R) : x = z := by sorry