proposition: Lemma ex_per_cong : forall A B C D X Y, A <> B -> X <> Y -> Col A B C -> ~Col A B D -> exists P, Per P C A /\ Cong P C X Y /\ OS A B P D.
proof: Proof. intros A B C D X Y HAB HXY HCol HNCol. destruct (l10_15 A B C D) as [Q [HQ1 HQ2]]; trivial. assert_diffs. destruct (segment_construction_3 C Q X Y) as [P [HP1 HP2]]; auto. exists P; repeat split; Cong. - destruct (eq_dec_points A C). subst; Perp. apply perp_per_1. apply perp_col1 with B; auto. assert_diffs; apply perp_sym, perp_col1 with Q; Col; Perp. - apply os_out_os with Q C; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop