proposition: Lemma coordinates_of_point : forall O E S U1 U2 P, Cs O E S U1 U2 -> exists X, exists Y, Cd O E S U1 U2 P X Y.
proof: Proof. intros O E S U1 U2 P HCs. assert (H := HCs); destruct H as [HDiff [HCong1 [HCong2 H]]]; clear H. assert (HSU1 : S <> U1) by (assert_diffs; auto). assert (HSU2 : S <> U2) by (assert_diffs; auto). destruct (exists_coord O E S U1 P HSU1 HCong1) as [PX [X HX]]. destruct (exists_coord O E S U2 P HSU2 HCong2) as [PY [Y HY]]. exists X; exists Y; split; auto. split; try (apply all_coplanar). split; [exists PX|exists PY]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths