proposition: Lemma l11_22a : forall A B C P A' B' C' P', TS B P A C /\ TS B' P' A' C' /\ CongA A B P A' B' P' /\ CongA P B C P' B' C' -> CongA A B C A' B' C'.
proof: Proof. intros. spliter. assert (A <> B /\ A' <> B' /\ P <> B /\ P' <> B' /\ C <> B /\ C' <> B'). unfold CongA in *. spliter. repeat split; assumption. assert(A <> C /\ A' <> C'). unfold TS in *. spliter. ex_and H12 T. ex_and H10 T'. split. intro. subst C. apply between_identity in H13. subst T. contradiction. intro. subst C'. apply between_identity in H14. subst T'. contradiction. spliter. assert(exists A'', Out B' A' A'' /\ Cong B' A'' B A). eapply segment_construction_3; auto. ex_and H11 A''. unfold TS in H. assert (~ Col A B P). spliter. assumption. spliter. ex_and H15 T. induction (eq_dec_points B T). subst T. assert(Bet A' B' C'). eapply l11_22_bet. apply H16. apply invert_two_sides. apply H0. split. apply H1. assumption. apply conga_line. assumption. auto. assumption. auto. assumption. assumption. induction(bet_dec P B T). assert(exists T'', Col B' P' T'' /\ (Out B' P' T'' <-> Out B P T) /\ Cong B' T'' B T). prolong P' B' T'' B T. exists T''. split. unfold Col. right; right. apply between_symmetry. assumption. split. split. intro. assert(Bet P' B' T'' /\ Out B' P' T''). split; assumption. apply (not_bet_and_out _ _ _)in H22. contradiction. intro. assert(Bet P B T /\ Out B P T). split; assumption. apply (not_bet_and_out _ _ _)in H22. contradiction. assumption. ex_and H19 T''. destruct H20. assert (B' <> T''). intro. subst T''. apply cong_symmetry in H21. apply cong_identity in H21. contradiction. assert(exists C'', Bet A'' T'' C'' /\ Cong T'' C'' T C). prolong A'' T'' C'' T C. exists C''. split; assumption. ex_and H24 C''. assert(CongA A B T A' B' T''). apply conga_comm. eapply l11_13. apply conga_comm. apply H1. assumption. auto. eapply out_to_bet. apply col_permutation_4. assumption. split. apply H22. assumption. assumption. auto. assert(CongA A B T A'' B' T''). eapply l11_10. apply H26. apply out_trivial. auto. apply out_trivial. auto. apply l6_6. assumption. apply out_trivial. auto. assert(Cong A T A'' T''). assert(HH:= l11_4_1 A B T A'' B' T'' H27). spliter. apply H32. split. apply out_trivial. auto. split. apply out_trivial. auto. split. apply out_trivial. intro. subst A''. absurde. split. apply out_trivial. assumption. split. apply cong_symmetry. assumption. apply cong_symmetry. assumption. assert(Cong A C A'' C''). eapply l2_11. apply H16. apply H24. assumption. apply cong_symmetry. assumption. assert(Cong C B C'' B'). apply (five_segment A A'' T T''); Cong. intro. subst T. apply H13. assumption. assert(CongA A B C A'' B' C''). apply cong3_conga. assumption. assumption. repeat split. apply cong_commutativity. apply cong_symmetry. assumption. assumption. apply cong_commutativity. assumption. assert(CongA C B T C'' B' T''). apply cong3_conga. assumption. auto. repeat split. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assert (CongA P B C P' B' C''). eapply l11_13. apply conga_comm. apply H32. apply between_symmetry. assumption. assumption. apply between_symmetry. eapply out_to_bet. eapply col_permutation_4. assumption. split. apply H22. assumption. assumption. assumption. assert(CongA P' B' C' P' B' C''). eapply conga_trans. apply conga_sym. apply H2. assumption. assert(Out B' C' C'' \/ TS P' B' C' C''). apply conga_cop__or_out_ts. assert (HH := H0); destruct HH as [HNCol]. apply coplanar_trans_1 with A'; Col. Cop. assert_diffs; apply coplanar_perm_19, col_cop__cop with A''; Col. exists T''. right. left. split; Col. assumption. induction H35. eapply l11_10. apply H31. apply out_trivial. auto. apply out_trivial. auto. assumption. assumption. assert(TS B' P' A'' C'). apply l9_2. eapply l9_5. eapply l9_2. eapply l9_5. apply H0. apply col_trivial_1. assumption. apply col_trivial_1. apply out_trivial. auto. apply invert_two_sides in H35. apply l9_2 in H35. assert(OS B' P' A'' C''). unfold OS. exists C'. split; assumption. assert (TS B' P' A'' C''). unfold TS. repeat split. intro. unfold TS in H0. assert (~ Col A' B' P'). spliter. assumption. spliter. apply H39. apply col_permutation_2. eapply (col_transitivity_1 _ A''). intro. subst A''. unfold Out in H11. spliter. absurde. apply col_permutation_4. assumption. apply out_col in H11. apply col_permutation_5. assumption. intro. unfold TS in H35. spliter. apply H35. assumption. exists T''. split. apply col_permutation_2. assumption. assumption. apply l9_9 in H38. contradiction. apply not_bet_out in H18. assert(exists T'', Col B' P' T'' /\ (Out B' P' T'' <-> Out B P T) /\ Cong B' T'' B T). assert (exists T'', Out B' P' T'' /\ Cong B' T'' B T). apply segment_construction_3. auto. assumption. ex_and H19 T''. exists T''. split. apply out_col in H19. assumption. split. split. intro. assumption. intro. assumption. assumption. ex_and H19 T''. destruct H20. assert (B' <> T''). intro. subst T''. apply cong_symmetry in H21. apply cong_identity in H21. contradiction. assert(exists C'', Bet A'' T'' C'' /\ Cong T'' C'' T C). prolong A'' T'' C'' T C. exists C''. split; assumption. ex_and H24 C''. assert(CongA A B T A' B' T''). eapply l11_10. apply H1. apply out_trivial. auto. apply l6_6. assumption. apply out_trivial. auto. apply l6_6. apply H22. assumption. assert(CongA A B T A'' B' T''). eapply l11_10. apply H26. apply out_trivial. auto. apply out_trivial. auto. apply l6_6. assumption. apply out_trivial. auto. assert(Cong A T A'' T''). assert(HH:= l11_4_1 A B T A'' B' T'' H27). spliter. apply H32. split. apply out_trivial. auto. split. apply out_trivial. assumption. split. apply out_trivial. intro. subst A''. absurde. split. apply out_trivial. assumption. split. apply cong_symmetry. assumption. apply cong_symmetry. assumption. assert(Cong A C A'' C''). eapply l2_11. apply H16. apply H24. assumption. apply cong_symmetry. assumption. assert(Cong C B C'' B'). apply (five_segment A A'' T T''); Cong. intro. apply H13. subst T. assumption. assert(CongA A B C A'' B' C''). apply cong3_conga. assumption. assumption. repeat split. apply cong_commutativity. apply cong_symmetry. assumption. assumption. apply cong_commutativity. assumption. assert(CongA C B T C'' B' T''). apply cong3_conga. assumption. auto. repeat split. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. assumption. eapply l11_10. apply H31. apply out_trivial. auto. apply out_trivial. auto. assumption. assert(Out B' C' C'' \/ TS P' B' C' C''). apply conga_cop__or_out_ts. assert (HH := H0); destruct HH as [HNCol]. apply coplanar_trans_1 with A'; Col. Cop. assert_diffs; apply coplanar_perm_19, col_cop__cop with A''; Col. exists T''. right. left. split; Col. apply conga_comm. eapply conga_trans. apply conga_comm. apply conga_sym. apply H2. eapply l11_10. apply H32. apply out_trivial. auto. assumption. apply out_trivial. intro. subst C''. apply cong_identity in H30. contradiction. apply H22. assumption. induction H33. assumption. assert(TS B' P' A'' C'). apply l9_2. eapply l9_5. eapply l9_2. eapply l9_5. apply H0. apply col_trivial_1. assumption. apply col_trivial_1. apply out_trivial. auto. assert(OS B' P' A'' C''). unfold OS. exists C'. split. assumption. apply invert_two_sides in H33. apply l9_2 in H33. assumption. assert (TS B' P' A'' C''). unfold TS. repeat split. intro. unfold TS in H34. spliter. apply H34. assumption. intro. unfold TS in H33. spliter. apply H37. apply col_permutation_5. assumption. exists T''. split. apply col_permutation_2. assumption. assumption. apply l9_9 in H36. contradiction. auto. apply col_permutation_3. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2