proposition: Lemma characterization_of_parallelism_F_bis : 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 =F= Bx) \/ ~ (Ay =F= By)) /\ (~ (Cx =F= Dx) \/ ~ (Cy =F= Dy)).
proof: Proof. assert (Nsat2 : ~ (-(2) =F= 0)). now prove_discr_for_powers_of_2. assert (Nsat4 : ~ (2 * (1 + 1) =F= 0)). now prove_discr_for_powers_of_2. assert (Nsatm4 : ~ (-(2 * (1 + 1)) =F= 0)). now prove_discr_for_powers_of_2. assert (Nsat8 : ~ (2 * (2 * (1 + 1)) =F= 0)). now prove_discr_for_powers_of_2. intros; rewrite characterization_of_parallelism_F_aux. split; [intro H; destruct H as [HAB [HCD [P [HP [Q [HQ HCol]]]]]]|]. { revert HCol; revert HQ; revert HP; revert HCD; revert HAB. setoid_rewrite characterization_of_neq_F_bis. setoid_rewrite characterization_of_midpoint_F. setoid_rewrite characterization_of_collinearity_F. 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] _. elim (coordinates_of_point_F P); intros [Px Py] _. elim (coordinates_of_point_F Q); intros [Qx Qy] _. intros HAB HCD [HPx HPy] [HQx HQy] HCol; split; [|split; assumption]. rewrite <- neg_and_eqF in HAB; rewrite <- neg_and_eqF in HCD. cut ((Ax - Bx) * (Cy - Dy) - (Ay - By) * (Cx - Dx) =F= 0 \/ ((Ax =F= Bx) /\ (Ay =F= By)) \/ ((Cx =F= Dx) /\ (Cy =F= Dy))); [intuition|]. scnf; try (clear HAB; clear HCD; repeat rewrite <- mulF__eq0; nsatz). clear HPx; clear HPy; clear HQx; clear HQy; clear HCol. destruct H as [[H1 H2] [H3 H4]]; elim H1; clear H1; [auto|intro H1]; elim H2; clear H2; [auto|intro H2]; elim H3; clear H3; [auto|intro H3]; elim H4; clear H4; [auto|intro H4; exfalso; rtauto]. } { destruct (symmetric_point_construction A C) as [P HP]; revert HP. destruct (midpoint_existence B P) as [Q HQ]; revert HQ. setoid_rewrite characterization_of_neq_F_bis. setoid_rewrite characterization_of_midpoint_F. setoid_rewrite characterization_of_collinearity_F. 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] _. intros HP HQ [HPar [HAB HCD]]; split; [assumption|split; [assumption|]]. exists P; revert HQ; revert HP. elim (coordinates_of_point_F P); intros [Px Py] _; intros HQ [HPx HPy]. split; [split; assumption|]; exists Q; revert HQ. elim (coordinates_of_point_F Q); intros [Qx Qy] _; intros [HQx HQy]. split; [split; assumption|]. rewrite <- neg_and_eqF in HAB; rewrite <- neg_and_eqF in HCD. cut ((Cx - Dx) * (Dy - Qy) - (Cy - Dy) * (Dx - Qx) =F= 0 \/ ((Ax =F= Bx) /\ (Ay =F= By)) \/ ((Cx =F= Dx) /\ (Cy =F= Dy))); [intuition|]. assert (Nsatm2 : ~ (2 =F= 0)) by prove_discr_for_powers_of_2. scnf; clear HAB; clear HCD; repeat rewrite <- mulF__eq0; try nsatz. decompose [and or] H; clear H; 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