proposition: Lemma l11_25_aux : forall P A B C A', InAngle P A B C -> ~ Bet A B C -> Out B A' A -> InAngle P A' B C.
proof: Proof. intros. unfold Out in H1. unfold InAngle in H. spliter. repeat split ; try assumption. induction H3. ex_and H6 X. assert(exists T, Bet A' T C /\ Bet X T B). eapply inner_pasch. apply H3. apply between_symmetry. assumption. ex_and H8 T. exists T. split. assumption. right. induction H7. subst B. contradiction. unfold Out in *. spliter. repeat split. intro. subst T. apply H0. apply between_symmetry. eapply outer_transitivity_between. apply between_symmetry. apply H8. assumption. auto. assumption. induction H11. left. eapply between_exchange4. apply between_symmetry. apply H9. assumption. eapply l5_3. apply between_symmetry. apply H9. assumption. ex_and H6 X. induction H7. subst X. contradiction. assert(exists T, Bet A' T C /\ Bet B X T). eapply outer_pasch. apply between_symmetry. apply H3. apply between_symmetry. assumption. ex_and H8 T. exists T. split. assumption. right. unfold Out in H7. spliter. repeat split. intro. subst T. apply between_identity in H9. subst X. absurde. assumption. induction H11. apply l5_1 with X; auto. right. eapply between_exchange4. apply H11. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2