proposition: Lemma characterization_of_equality_F : forall A B, A = B <-> let (Ac, _) := coordinates_of_point_F A in let (Ax, Ay) := Ac in let (Bc, _) := coordinates_of_point_F B in let (Bx, By) := Bc in Ax =F= Bx /\ Ay =F= By.
proof: Proof. intros A B; unfold EqF. elim (coordinates_of_point_F A); intros [[Ax HAx] [Ay HAy]] HAc. elim (coordinates_of_point_F B); intros [[Bx HBx] [By HBy]] HBc. rewrite (eq_points_coordinates O E SS U1 U2 A Ax Ay B Bx By HAc HBc). split; intro; spliter; split; treat_equalities; simpl; auto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems