proposition: Lemma point_of_coordinates_on_an_axis : forall O E S U1 U2 X, Cs O E S U1 U2 -> Col O E X -> O <> X -> exists P, Cd O E S U1 U2 P X O.
proof: Proof. intros O E S U1 U2 X HCs HCol HOX. assert (H := HCs); destruct H as [HDiff [HCong1 [HCong2 H]]]; clear H. destruct (l4_14 O E X S U1 HCol HCong1) as [P HP]. exists P; split; auto. destruct HCs as [H [H' [H'' HPer]]]; clear H; clear H'; clear H''. split; try apply all_coplanar. assert_diffs; split; [exists P|exists S]; repeat (split; Cong); [right; split; try apply l4_13 with O E X; Col|]. left; split; Col. apply per_perp in HPer; auto. apply perp_col0 with S U1; Col; Perp; [unfold Cong_3 in *; spliter; assert_diffs|apply l4_13 with O E X]; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths