proposition: Lemma characterization_of_perpendicularity_F_bis : forall A B C D, Perp 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) * (Cx - Dx) + (Ay - By) * (Cy - Dy) =F= OF /\ (~ (Ax =F= Bx) \/ ~ (Ay =F= By)) /\ (~ (Cx =F= Dx) \/ ~ (Cy =F= Dy)).
proof: Proof. intros; split; [intro H; destruct H as [X [HAB [HCD [HC1 [HC2 HPer]]]]]|]. { assert (HA : Col A A B) by Col; assert (HB : Col B A B) by Col. assert (HC : Col C C D) by Col; assert (HD : Col D C D) by Col. assert (HPer1:=HPer A C HA HC); assert (HPer2:=HPer B C HB HC); clear HC. assert (HPer3:=HPer A D HA HD); assert (HPer4:=HPer B D HB HD); clear HD. clear HA; clear HB; clear HPer; revert HPer4; revert HPer3; revert HPer2; revert HPer1; revert HC2; revert HC1; revert HCD; revert HAB. setoid_rewrite characterization_of_neq_F_bis. setoid_rewrite characterization_of_collinearity_F. setoid_rewrite characterization_of_right_triangle_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 X); intros [Xx Xy] _. intros; split; [nsatz|split; assumption]. } { unfold Perp, Perp_at; intro HPerp. assert (HX : ~ Par A B C D); revert HPerp. { intro H; assert (HAB : A <> B); revert H. { rewrite characterization_of_neq_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] _. intro; spliter; auto. } rewrite characterization_of_parallelism_F_bis. rewrite characterization_of_neq_F in HAB; revert HAB. 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 HAB [HPerp [_ HCD]]; intros [HPar _]; apply HAB. cut ((Ax - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) =F= 0 \/ ((Cx =F= Dx) /\ (Cy =F= Dy))); [intuition|]. rewrite <- neg_and_eqF in HCD; scnf; [| |exfalso; rtauto]; clear HCD; repeat rewrite <- mulF__eq0; nsatz. } setoid_rewrite characterization_of_neq_F_bis. setoid_rewrite characterization_of_collinearity_F. setoid_rewrite characterization_of_right_triangle_F. apply not_par_inter_exists in HX; destruct HX as [X [H1 H2]]. revert H2; revert H1; 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 H1 H2 [HPerp [HAB HCD]]. exists X; repeat split; auto; intros U V; revert H2; revert H1. elim (coordinates_of_point_F X); intros [Xx Xy] _; intros H1 H2. elim (coordinates_of_point_F U); intros [Ux Uy] _. elim (coordinates_of_point_F V); intros [Vx Vy] _; intros H3 H4. rewrite <- neg_and_eqF in HAB; rewrite <- neg_and_eqF in HCD. cut ((Ux - Xx) * (Xx - Vx) + (Uy - Xy) * (Xy - Vy) =F= 0 \/ ((Ax =F= Bx) /\ (Ay =F= By)) \/ ((Cx =F= Dx) /\ (Cy =F= Dy))); [intuition|]. scnf; try solve [clear HAB; clear HCD; repeat rewrite <- mulF__eq0; nsatz]. clear HPerp; clear H1; clear H2; clear H3; clear H4. 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]. } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems