proposition: Lemma characterization_of_neq_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 - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) =F= OF).
proof: Proof. intros; rewrite characterization_of_equality_F_bis. elim (coordinates_of_point_F A); intros [Ax Ay] _. elim (coordinates_of_point_F B); intros [Bx By] _; simpl; split; 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