proposition: Lemma in_angle_out : forall A B C P, Out B A C -> InAngle P A B C -> Out B A P.
proof: Proof. intros. unfold InAngle in H0. spliter. ex_and H3 X. induction H4. subst X. assert( Bet A B C /\ Out B A C). split; assumption. apply not_bet_and_out in H4. contradiction. unfold Out in *. spliter. induction H8; induction H6. repeat split; try assumption. left. assert(Bet B A X). eapply between_inner_transitivity. apply H8. apply H3. eapply between_exchange4. apply H9. assumption. repeat split; try assumption. assert(Bet B A X). eapply between_inner_transitivity. apply H8. assumption. eapply l5_3. apply H9. assumption. repeat split; try assumption. assert(Bet B X A). eapply between_exchange2. apply H8. apply between_symmetry. assumption. apply l5_1 with X; auto. repeat split; auto. right. assert(Bet B X A). eapply between_exchange2. apply H8. apply between_symmetry. assumption. eapply between_exchange4. apply H6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2