proposition: Lemma orth_at2_tsp__ts : forall A B C X Y P Q, P <> Q -> Orth_at P A B C P X -> Orth_at Q A B C Q Y -> TSP A B C X Y -> TS P Q X Y.
proof: Proof. intros A B C X Y P Q HPQ HP HQ [HX [HY [T [HT HBet]]]]. assert (HP1 := HP). apply orth_at_chara in HP1; spliter. assert (HQ1 := HQ). apply orth_at_chara in HQ1; spliter. repeat split. intro; apply HX, col_cop2__cop with P Q; Col. intro; apply HY, col_cop2__cop with P Q; Col. exists T; split; [|assumption]. destruct (symmetric_point_construction X P) as [X']. destruct (symmetric_point_construction Y Q) as [Y']. assert (Cong T X T X') by (apply per_double_cong with P; auto). assert (Cong T Y T Y') by (apply per_double_cong with Q; auto). apply col_permutation_4, bet_col, l7_22 with X Y X' Y'; trivial. apply (l4_6 X T Y); repeat split; Cong. assert (~ Col A B C) by (apply ncop__ncol with X, HX). apply mid2_orth_at2__cong with A B C P Q; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2