proposition: Lemma characterization_of_parallelism_F : forall A B C D, Par A B C D <-> 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 let (Cc, _) := coordinates_of_point_F C in let (Cx, Cy) := Cc in let (Dc, _) := coordinates_of_point_F D in let (Dx, Dy) := Dc in (Ax - Bx) * (Cy - Dy) - (Ay - By) * (Cx - Dx) =F= 0 /\ ~ ((Ax - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) =F= OF) /\ ~ ((Cx - Dx) * (Cx - Dx) + (Cy - Dy) * (Cy - Dy) =F= OF).
proof: Proof. intros; rewrite characterization_of_parallelism_F_bis. elim (coordinates_of_point_F A); intros [Ax Ay] _. elim (coordinates_of_point_F B); intros [Bx By] _. elim (coordinates_of_point_F C); intros [Cx Cy] _. elim (coordinates_of_point_F D); intros [Dx Dy] _. setoid_rewrite <- characterization_of_equality_F_aux. setoid_rewrite <- neg_and_eqF; tauto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems