proposition: Lemma ts2__inangle : forall A B C P, TS A C B P -> TS B P A C -> InAngle P A B C.
proof: Proof. intros A B C P HTS1 HTS2. destruct (ts2__ex_bet2 A B C P) as [X [HBet1 HBet2]]; trivial. apply ts_distincts in HTS2; spliter. repeat split; auto. exists X; split; trivial. right; apply bet_out; auto. intro; subst X. apply (two_sides_not_col A C B P HTS1); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2