proposition: Lemma l11_50_2 : forall A B C A' B' C', ~ Col A B C -> CongA B C A B' C' A' -> CongA A B C A' B' C' -> Cong A B A' B' -> Cong A C A' C' /\ Cong B C B' C' /\ CongA C A B C' A' B'.
proof: Proof. intros. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B'). unfold CongA in H1. spliter. repeat split; assumption. spliter. assert(exists C'', Out B' C'' C' /\ Cong B' C'' B C). apply l6_11_existence. assumption. auto. ex_and H7 C''. assert(B' <> C''). unfold Out in H7. spliter. auto. assert(~Col A' B' C'). eapply ncol_conga_ncol. apply H. assumption. assert(~Col A' B' C''). intro. apply H10. apply out_col in H7. eapply col_permutation_2. eapply (col_transitivity_1 _ C''). assumption. assumption. apply col_permutation_1. assumption. assert(HH:=l11_4_1 A B C A' B' C' H1). spliter. assert(Cong A C A' C''). apply H16. repeat (split; [Out|]); Cong. assert(Cong_3 B C A B' C'' A'). repeat split; Cong. assert(CongA B C A B' C'' A'). apply cong3_conga. auto. apply not_col_distincts in H. spliter. auto. assumption. assert(CongA B' C' A' B' C'' A'). eapply conga_trans. apply conga_sym. apply H0. assumption. apply not_col_distincts in H. apply not_col_distincts in H10. spliter. clear H16. induction(eq_dec_points C' C''). induction (eq_dec_points C' C''). subst C''. split. assumption. split. apply cong_symmetry. assumption. assert(Cong_3 C A B C' A' B'). repeat split. apply cong_commutativity. assumption. apply cong_commutativity. apply cong_symmetry. assumption. assumption. apply cong3_conga. auto. auto. assumption. apply False_ind. apply H27. assumption. assert(~ Col C'' C' A'). intro. apply H10. apply col_permutation_1. eapply col_transitivity_1. apply H16. apply col_permutation_4. assumption. apply col_permutation_3. apply out_col. assumption. apply not_col_distincts in H27. spliter. unfold Out in H7. spliter. induction H32. assert(HH:=l11_41). assert(HH1:=l11_41 C'' C' A' B' H27 (between_symmetry _ _ _ H32) H7). spliter. assert(CongA B' C' A' C'' C' A'). eapply (l11_10 B' C' A' B' C' A'). apply conga_refl. auto. assumption. apply out_trivial. assumption. apply out_trivial. auto. apply bet_out. auto. apply between_symmetry. assumption. apply out_trivial. auto. assert(LtA B' C' A' A' C'' B'). eapply conga_preserves_lta. apply conga_sym. apply H35. apply conga_refl. auto. auto. assumption. unfold LtA in H36. spliter. apply conga_right_comm in H20. contradiction. assert(~Col C' C'' A'). intro. apply H27. apply col_permutation_4. assumption. assert(HH1:=l11_41 C' C'' A' B' H33 (between_symmetry _ _ _ H32) H15). spliter. assert(CongA B' C'' A' C' C'' A'). apply out2__conga. apply bet_out. auto. apply between_symmetry. assumption. apply out_trivial. auto. assert(LtA B' C'' A' A' C' B'). eapply conga_preserves_lta. apply conga_sym. apply H36. apply conga_refl. auto. auto. assumption. unfold LtA in H37. spliter. apply conga_sym in H20. apply conga_right_comm in H20. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2