proposition: Lemma two_sides_in_angle : forall A B C P P', B <> P' -> TS B P A C -> Bet P B P' -> InAngle P A B C \/ InAngle P' A B C.
proof: Proof. intros. unfold TS in H0. spliter. ex_and H3 T. assert(A <> B). intro. subst A. apply H0. apply col_trivial_1. assert(C <> B). intro. subst C. apply H2. apply col_trivial_1. induction (eq_dec_points B T). subst T. left. repeat split. assumption. assumption. intro. subst B. Col. exists B. split. assumption. left. reflexivity. assert(P <> B /\ T <> B). split. intro. subst B. Col. auto. spliter. assert(HH:= or_bet_out P B T). induction HH. right. unfold InAngle. repeat split; try assumption. unfold Out in H1. spliter. auto. exists T. split. assumption. right. unfold Out. repeat split. auto. auto. apply (l5_2 P); auto. induction H10. left. unfold InAngle. repeat split; try assumption. auto. exists T. split. assumption. right. apply l6_6. assumption. apply col_permutation_3 in H3. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2