proposition: Lemma l11_25 : forall P A B C A' C' P', InAngle P A B C -> Out B A' A -> Out B C' C -> Out B P' P -> InAngle P' A' B C'.
proof: Proof. intros. induction (bet_dec A B C). repeat split. unfold Out in H0. spliter. assumption. unfold Out in H1. spliter. assumption. unfold Out in H2. spliter. assumption. exists B. split. eapply bet_out_out_bet. apply H3. apply l6_6. assumption. apply l6_6. assumption. left. reflexivity. assert(InAngle P A' B C). eapply l11_25_aux. apply H. assumption. assumption. assert(InAngle P A' B C'). apply l11_24. eapply l11_25_aux. apply l11_24. apply H4. intro. apply H3. apply between_symmetry. eapply bet_out_out_bet. apply H5. apply out_trivial. unfold InAngle in H. spliter. auto. assumption. assumption. unfold InAngle in H5. spliter. ex_and H8 X. induction H9. subst X. apply False_ind. apply H3. eapply bet_out_out_bet. apply H8. assumption. assumption. repeat split. assumption. assumption. intro. subst P'. unfold Out in H2. spliter. absurde. exists X. split. assumption. right. eapply l6_7. apply H9. apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2