proposition: Lemma l11_52 : forall A B C A' B' C', CongA A B C A' B' C' -> Cong A C A' C' -> Cong B C B' C' -> Le B C A C -> Cong B A B' A' /\ CongA B A C B' A' C' /\ CongA B C A B' C' A'.
proof: Proof. intros. apply conga_distinct in H. spliter. assert(Cong B A B' A'). induction(col_dec A B C). unfold Col in H7. induction H7. assert(Bet A' B' C'). eapply bet_conga__bet. apply H7. assumption. apply cong_commutativity. eapply l4_3. apply H7. apply H8. assumption. assumption. induction H7. assert(Out B' A' C'). eapply l11_21_a. apply bet_out. apply H4. apply H7. apply conga_left_comm. assumption. unfold Out in H8. spliter. induction H10. assert(Le B' C' A' C'). eapply l5_6. repeat split. apply H2. assumption. assumption. assert(B'=A'). eapply bet_le_eq. apply H10. assumption. subst B'. absurde. eapply l2_11. apply H7. apply H10. assumption. Cong. assert(B = A). eapply bet_le_eq. apply between_symmetry. apply H7. assumption. subst B. absurde. assert(exists A'', Out B' A'' A' /\ Cong B' A'' B A). apply l6_11_existence. assumption. auto. ex_and H8 A''. assert(CongA A' B' C' A'' B' C'). apply out2__conga. assumption. apply out_trivial. auto. assert(CongA A B C A'' B' C'). eapply l11_10. apply H. apply out_trivial. auto. apply out_trivial. auto. assumption. apply out_trivial. auto. assert(Cong A'' C' A C). eapply cong2_conga_cong. apply conga_sym. apply H11. Cong. Cong. assert(Cong_3 A'' B' C' A B C). repeat split; Cong. assert(Cong A'' C' A' C'). eapply cong_transitivity. apply H12. assumption. assert(~Col A' B' C'). eapply ncol_conga_ncol. apply H7. assumption. assert(~Col A'' B' C'). intro. apply H15. apply col_permutation_2. eapply (col_transitivity_1 _ A''). intro. subst A''. unfold Out in H8. spliter. absurde. Col. Col. induction(eq_dec_points A'' A'). subst A''. unfold Cong_3 in H13. spliter. Cong. unfold Out in H8. spliter. induction H19. assert(HH:= l11_41 A'' B' C' A' H16 H19 H17). spliter. assert(Cong A' C' A'' C'). apply (cong_transitivity _ _ A C). Cong. unfold Cong_3 in H13. spliter. Cong. assert(~ Col A'' C' A'). intro. apply H15. apply (col_transitivity_1 _ A''); Col. assert (HH:= l11_44_1 A'' C' A' H23). destruct HH. apply cong_commutativity in H22. apply cong_symmetry in H22. apply H25 in H22. assert(~ Col B' C' A''). Col. assert(CongA B' A' C' A'' A' C'). apply out2__conga. apply bet_out; Between. apply out_trivial. intro. subst C'. apply H15. apply col_trivial_3. assert(~Col B' C' A'). Col. assert(HH:=l11_44_2 B' C' A' H28). destruct HH. assert(Lt C' A' C' B'). apply H29. apply (conga_preserves_lta A'' B' C' C' A'' A'). apply conga_right_comm. apply conga_sym. apply H10. eapply conga_trans. apply H22. apply conga_comm. apply conga_sym. assumption. assumption. assert(Lt C' A'' C' B'). unfold Lt in H31. spliter. unfold Lt. split. eapply l5_6. apply H31. Cong. Cong. intro. apply H32. eapply cong_transitivity. apply cong_commutativity. apply cong_symmetry. apply H14. assumption. unfold Lt in H32. spliter. assert(Le C A C B). eapply l5_6. repeat split. apply H32. apply cong_commutativity. assumption. Cong. assert(Cong C A C B). apply le_anti_symmetry. assumption. apply le_comm. assumption. apply False_ind. apply H33. apply cong_symmetry. eapply cong_transitivity. apply cong_commutativity. apply cong_symmetry. apply H1. eapply cong_transitivity. apply cong_symmetry. apply H35. Cong. assert(A' <> A''). auto. assert(HH:= l11_41 A' B' C' A'' H15 H19 H20). spliter. assert(Cong A' C' A'' C'). apply (cong_transitivity _ _ A C). Cong. unfold Cong_3 in H13. spliter. Cong. assert(~ Col A'' C' A'). intro. apply H15. eapply (col_transitivity_1 _ A'' ); Col. assert (HH:= l11_44_1 A'' C' A' H24 ). destruct HH. apply cong_commutativity in H23. apply cong_symmetry in H23. apply H26 in H23. assert(~Col B' C' A''). Col. assert(CongA B' A'' C' A' A'' C'). apply out2__conga. apply bet_out; Between. apply out_trivial. intro. subst C'. apply H16. apply col_trivial_3. assert(~Col B' C' A''). Col. assert(HH:=l11_44_2 B' C' A'' H29). destruct HH. assert(Lt C' A'' C' B'). apply H30. apply (conga_preserves_lta A' B' C' C' A' A''). apply conga_right_comm. apply conga_sym. apply conga_sym. apply H10. eapply conga_trans. apply conga_sym. apply H23. apply conga_comm. apply conga_sym. assumption. assumption. assert(Lt C' A' C' B'). unfold Lt in H32. spliter. unfold Lt. split. eapply l5_6. apply H32. Cong. Cong. intro. apply H33. eapply cong_transitivity. apply cong_commutativity. apply H14. assumption. unfold Lt in H33. spliter. assert(Le C A C B). eapply l5_6. repeat split. apply H32. apply cong_commutativity. assumption. Cong. assert(Cong C A C B). apply le_anti_symmetry. assumption. apply le_comm. assumption. apply False_ind. apply H34. apply cong_symmetry. eapply cong_transitivity. apply cong_commutativity. apply cong_symmetry. apply H1. eapply cong_transitivity. apply cong_symmetry. apply H36. Cong. assert(Cong_3 A B C A' B' C'). repeat split; Cong. split. assumption. split. apply cong3_conga. auto. intro. subst C. apply le_zero in H2. subst B. absurde. auto with cong3. apply cong3_conga. auto. intro. subst C. apply le_zero in H2. subst B. absurde. auto with cong3. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2