Concentric_Circles_do_not_Intersect
Provedeuclidgeometryproofwiki
If two circles are concentric with different radii, they do not intersect.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Concentric_Circles_do_not_Intersect (cx cy r1 r2 : ℝ) (hr1 : r1 > 0) (hr2 : r2 > 0) (hne : r1 ≠ r2) : ¬∃ x y : ℝ, (x - cx) ^ 2 + (y - cy) ^ 2 = r1 ^ 2 ∧ (x - cx) ^ 2 + (y - cy) ^ 2 = r2 ^ 2 := by sorry
Source