proposition: Lemma os_ts__inangle : forall A B C P, TS B P A C -> OS B A C P -> InAngle P A B C.
proof: Proof. intros A B C P Hts Hos. assert(HNCol : ~ Col A B P) by (destruct Hts as []; Col). assert(~ Col B A C) by (apply (one_side_not_col123 _ _ _ P); auto). assert (HP' := symmetric_point_construction P B). destruct HP' as [P']. assert_diffs. assert(~ Col B A P') by (intro; apply HNCol; ColR). assert(HUn := two_sides_in_angle A B C P P'). destruct HUn as [|Habs]; Between. exfalso. apply in_angle_one_side in Habs; Col. apply l9_9_bis in Habs. apply Habs. apply invert_two_sides; apply l9_2. apply (l9_8_2 _ _ P); Side. repeat split; Col; exists B; split; Col; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2