proposition: Lemma tsp_dec : forall A B C X Y, TSP A B C X Y \/ ~ TSP A B C X Y.
proof: Proof. intros A B C X Y. destruct (cop_dec A B C X) as [|HX]. right; intros [Ha]; apply Ha; assumption. destruct (cop_dec A B C Y) as [|HY]. right; intros [_ [Ha]]; apply Ha; assumption. destruct (l11_62_existence_bis A B C X HX) as [P HP]. destruct (l11_62_existence_bis A B C Y HY) as [Q HQ]. assert (HP1 := HP). apply orth_at_chara in HP1; spliter. assert (HQ1 := HQ). apply orth_at_chara in HQ1; spliter. destruct (eq_dec_points P Q). { subst Q; clear HQ; destruct (bet_dec X P Y) as [|HNBet]. left; repeat split; trivial; exists P; split; trivial. right; intro HQ; apply HNBet. destruct HQ as [_ [_ [Q [HQ HBet]]]]. replace P with Q; [assumption|]. apply l8_8, (col_per2__per X Y); try (apply l8_2); Col. intro; treat_equalities; auto. } destruct (two_sides_dec P Q X Y) as [HT|HNTS]. left; apply cop2_ts__tsp with P Q; assumption. right; intro; apply HNTS, (orth_at2_tsp__ts A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2