proposition: Lemma in_angle_one_side : forall A B C P, ~ Col A B C -> ~ Col B A P -> InAngle P A B C -> OS A B P C.
proof: Proof. intros. unfold InAngle in H1. spliter. ex_and H4 X. induction H5. subst X. apply False_ind. apply H. unfold Col. left. assumption. unfold OS. prolong C A C' C A. exists C'. assert(TS A B X C'). repeat split. intro. apply H0. eapply (col_transitivity_1 _ X). intro. subst X. apply H. left. assumption. eapply (col_transitivity_1 _ A). auto. apply col_permutation_3. assumption. apply col_trivial_2. apply out_col. assumption. intro. apply H. eapply (col_transitivity_1 _ C'). intro. subst C'. apply cong_symmetry in H7. apply cong_identity in H7. subst C. apply H. apply col_trivial_3. apply col_permutation_4. assumption. unfold Col. right; right. assumption. exists A. split. apply col_trivial_1. eapply between_exchange3 with C; Between. split. apply l9_5 with X B; Col. repeat split. intro. apply H. apply col_permutation_1. assumption. intro. apply H. eapply (col_transitivity_1 _ C'). intro. subst C'. unfold TS in H8. spliter. apply H10. apply col_trivial_1. apply col_permutation_4. assumption. unfold Col. right; right. assumption. exists A. split. apply col_trivial_1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2