proposition: Lemma bet_in_angle_bet : forall A B C P, Bet A B P -> InAngle P A B C -> Bet A B C.
proof: Proof. intros. unfold InAngle in H0. spliter. ex_and H3 X. induction H4. subst X. assumption. unfold Out in H4. spliter. induction H6. assert(Bet A X P). eapply between_exchange2. apply H. assumption. assert(Bet A P C \/ Bet A C P). apply (l5_1 _ X). intro. subst X. assert(A = B). eapply between_equality. apply H. assumption. contradiction. assumption. assumption. induction H8. eapply between_exchange4. apply H. assumption. assert(Bet A B X). eapply between_inner_transitivity. apply H. assumption. eapply between_exchange4. apply H9. assumption. assert(Bet A B X). eapply outer_transitivity_between. apply H. assumption. auto. eapply between_exchange4. apply H7. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2