proposition: Lemma in_angle_trans : forall A B C D E, InAngle C A B D -> InAngle D A B E -> InAngle C A B E.
proof: Proof. intros. assert(HA1 :=H). assert(HA2:= H0). unfold InAngle in H. unfold InAngle in H0. spliter. ex_and H3 DD. ex_and H6 CC. induction H8; induction H7. subst CC. subst DD. apply in_angle_line; assumption. subst CC. assert(Bet A B E). eapply bet_in_angle_bet. apply H6. assumption. apply in_angle_line; assumption. subst DD. apply in_angle_line; assumption. assert(InAngle C A B DD). eapply l11_25. apply HA1. apply out_trivial. auto. assumption. apply out_trivial. auto. unfold InAngle in H9. spliter. ex_and H12 CC'. induction H13. subst CC'. assert(Bet A B E). eapply between_exchange4. apply H12. assumption. apply in_angle_line; assumption. apply l11_25 with CC' A E; [|apply out_trivial..|apply l6_6]; auto. repeat split; auto. unfold Out in H13. spliter. auto. exists CC'. split. eapply between_exchange4. apply H12. assumption. right. apply out_trivial. unfold Out in H13. spliter. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2