proposition: Lemma point_of_coordinates_origin : forall O E S U1 U2, Cs O E S U1 U2 -> Cd O E S U1 U2 S O O.
proof: Proof. intros O E S U1 U2 HCs. split; auto. split; try apply all_coplanar. destruct HCs as [HDiff [HCong1 [HCong2 H]]]; clear H. assert_diffs; split; exists S; repeat (split; Col; Cong). Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths