proposition: Lemma in_angle_two_sides : forall A B C P, ~ Col B A P -> ~ Col B C P -> InAngle P A B C -> TS P B A C.
proof: Proof. intros. unfold InAngle in H1. spliter. ex_and H4 X. induction H5. subst X. unfold TS. repeat split. intro. apply H. apply col_permutation_2. assumption. intro. apply H0. apply col_permutation_2. assumption. exists B. split. apply col_trivial_3. assumption. repeat split. intro. apply H. apply col_permutation_2. assumption. intro. apply H0. apply col_permutation_2. assumption. exists X. split. apply out_col in H5. apply col_permutation_1. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2