proposition: Lemma l11_30 : forall A B C D E F A' B' C' D' E' F', LeA A B C D E F -> CongA A B C A' B' C' -> CongA D E F D' E' F' -> LeA A' B' C' D' E' F'.
proof: Proof. intros. assert(HH:=H). apply l11_29_a in H. ex_and H Q. apply l11_29_b. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B' /\ D <> E /\ F <> E /\ D' <> E' /\ F' <> E'). unfold CongA in *. spliter. repeat split; assumption. spliter. assert(Hi:=or_bet_out A' B' C'). induction Hi. prolong A' B' Q' A' B'. exists Q'. assert(B' <> Q'). intro. subst Q'. apply cong_symmetry in H13. apply cong_identity in H13. contradiction. assert(A' <> Q'). intro. subst Q'. apply between_identity in H12. contradiction. assert(CongA A' B' Q' A' B' C'). apply conga_line; try assumption. auto. split. apply in_angle_line; try assumption. auto. assert(Bet A B C). eapply bet_conga__bet. apply H11. apply conga_sym. assumption. assert(Bet A B Q). eapply lea_line. apply H17. apply l11_29_b. exists Q. split. assumption. apply conga_refl. assumption. unfold CongA in H2. spliter. assumption. assert(Bet D E F). eapply bet_conga__bet. apply H18. assumption. assert (Bet D' E' F'). eapply bet_conga__bet. apply H19. assumption. eapply conga_line; try assumption. auto. induction H11. assert(exists Q', CongA D' E' F' A' B' Q'). eapply angle_construction_3; assumption. ex_and H12 Q'. exists Q'. split. apply col_in_angle; try assumption. unfold CongA in H13. spliter. assumption. left. assumption. apply conga_sym. assumption. assert(Hi:=or_bet_out D' E' F'). induction Hi. assert(exists Q', CongA D' E' F' A' B' Q'). eapply angle_construction_3; try assumption. ex_and H13 Q'. exists Q'. assert(Bet A' B' Q'). eapply bet_conga__bet. apply H12. assumption. split. apply in_angle_line; try assumption. unfold CongA in H14. spliter. assumption. apply conga_sym. assumption. induction H12. assert(exists Q', CongA D' E' F' A' B' Q'). eapply angle_construction_3; try assumption. ex_and H13 Q'. exists Q'. assert(Out B' A' Q'). eapply l11_21_a. apply H12. assumption. assert(CongA A B Q D' E' F'). eapply conga_trans. apply H2. assumption. assert(Out B A Q). eapply l11_21_a. apply H12. apply conga_sym. assumption. assert(Out B A C). eapply in_angle_out. apply H16. assumption. assert(Out B' A' C'). eapply l11_21_a. apply H17. assumption. split. apply out321__inangle. apply out_distinct in H13. spliter. auto. assumption. apply conga_sym. assumption. assert(exists QQ, CongA D' E' F' A' B' QQ /\ OS A' B' QQ C'). eapply angle_construction_1. assumption. assumption. ex_and H13 Q'. exists Q'. split. apply (conga_preserves_in_angle A B Q C); trivial. eapply conga_trans. apply H2. eapply conga_trans. apply H1. assumption. apply one_side_symmetry. assumption. apply conga_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2