proposition: Lemma exists_coord : forall O E S U P, S <> U -> Cong O E S U -> exists PX, exists X, Projp P PX S U /\ Cong_3 O E X S U PX.
proof: Proof. intros O E S U P HSU HCong. destruct (exists_projp S U P HSU) as [PX Hprojp]. assert (HCol : Col S U PX) by (destruct Hprojp as [H' H]; induction H; spliter; treat_equalities; Col). destruct (l4_14 S U PX O E) as [X HCong']; Cong. exists PX; exists X; auto with cong. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths