proposition: Lemma point_of_coordinates : forall O E S U1 U2 X Y, Cs O E S U1 U2 -> Col O E X -> Col O E Y -> exists P, Cd O E S U1 U2 P X Y.
proof: Proof. intros O E S U1 U2 X Y HCs HCol1 HCol2. elim (eq_dec_points O X); intro HOX; elim (eq_dec_points O Y); intro HOY; treat_equalities; [exists S; apply point_of_coordinates_origin| destruct (point_of_coordinates_on_an_axis O E S U2 U1 Y) as [P HP]; try apply grid_exchange_axes; try (exists P; apply coord_exchange_axes)| apply point_of_coordinates_on_an_axis|]; auto. assert (H := HCs); destruct H as [HDiff [HCong1 [HCong2 H]]]; clear H. destruct (l4_14 O E X S U1 HCol1 HCong1) as [PX HPX]. destruct (l4_14 O E Y S U2 HCol2 HCong2) as [PY HPY]. destruct (perp_exists PX S U1) as [PX' HPerp1]; [assert_diffs; auto|]. destruct (perp_exists PY S U2) as [PY' HPerp2]; [assert_diffs; auto|]. assert (HPerp3 : Perp PX PX' PY PY'). { apply par_perp__perp with S U2; Perp. apply l12_9_2D with S U1; Perp. destruct HCs as [H [H' [H'' HPer]]]; clear H; clear H'; clear H''. assert_diffs; apply per_perp in HPer; Perp. } assert (H := HPerp3); destruct H as [P HP]; exists P; split; auto. split; try apply all_coplanar. split; [exists PX|exists PY]; split; Cong. { assert_diffs; split; auto. left; split; [apply l4_13 with O E X; Col|]. unfold Perp_at in *; spliter; apply perp_col0 with PX PX'; Col. assert (HPYS : PY <> S) by (unfold Cong_3 in *; spliter; assert_diffs; auto). intro; treat_equalities; apply HPYS. apply l6_21 with S U1 U2 S; Col; [destruct HCs as [H' [H'' [H''' HPer]]]; apply perp_not_col; assert_diffs; apply per_perp in HPer; Perp| |apply l4_13 with E O Y; try apply cong_3_swap; Col]. assert (HPar : Par S U1 PY PY') by (apply l12_9_2D with P PX'; Perp). elim HPar; clear HPar; intro HParS; [|spliter; ColR]. exfalso; apply HParS; exists P; split; Col. apply l4_13 with X O E; try (apply cong_3_swap; apply cong_3_swap_2); Col. } { assert_diffs; split; auto. left; split; [apply l4_13 with O E Y; Col|]. unfold Perp_at in *; spliter; apply perp_col0 with PY PY'; Col. assert (HPXS : PX <> S) by (unfold Cong_3 in *; spliter; assert_diffs; auto). intro; treat_equalities; apply HPXS. apply l6_21 with S U2 U1 S; Col; [destruct HCs as [H' [H'' [H''' HPer]]]; apply perp_not_col; assert_diffs; apply per_perp in HPer; Perp| |apply l4_13 with E O X; try apply cong_3_swap; Col]. assert (HPar : Par S U2 PX PX') by (apply l12_9_2D with P PY'; Perp). elim HPar; clear HPar; intro HParS; [|spliter; ColR]. exfalso; apply HParS; exists P; split; Col. apply l4_13 with Y O E; try (apply cong_3_swap; apply cong_3_swap_2); Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths