Theorem: same_len_pts_coincide_iff (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
hlen : length a b = length c d
⊢ a = b ↔ c = d
Tactic:
rw [← @length_eq_zero_iff i a b, ← @length_eq_zero_iff i c d, hlen]
State after:
no goals