proposition: Lemma ex_conga_ts : forall A B C A' B' P, ~ Col A B C -> ~ Col A' B' P -> exists C' : Tpoint, CongA A B C A' B' C' /\ TS A' B' C' P.
proof: Proof. intros A B C A' B' P HNCol HNCol'. assert (HP' : exists P', Midpoint A' P P') by (apply symmetric_point_construction). destruct HP' as [P' HMid]. assert (~ Col A' B' P'). { intro HCol. apply HNCol'. assert (Col A' P P') by (apply midpoint_col; auto). apply (col3 A' P'); Col. intro; treat_equalities; Col. } assert (HC' : exists C', CongA A B C A' B' C' /\ OS A' B' C' P'). apply (angle_construction_1 A B C A' B' P'); auto. destruct HC' as [C' [HConga HOne]]. exists C'. split; auto. apply (l9_8_2 A' B' P'); Side. split; Col; split; Col. exists A'. split; Col. destruct HMid; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2