proposition: Lemma characterization_of_neq_F_bis : 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; rewrite characterization_of_equality_F; unfold EqF. elim (coordinates_of_point_F A); intros [[Ax HAx] [Ay HAy]] _. elim (coordinates_of_point_F B); intros [[Bx HBx] [By HBy]] _. simpl; split; intro; spliter; [|intuition]. destruct (eq_dec_points Ax Bx); destruct (eq_dec_points Ay By); intuition. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems