proposition: Lemma l11_50_1 : forall A B C A' B' C', ~ Col A B C -> CongA B A C B' A' C' -> CongA A B C A' B' C' -> Cong A B A' B' -> Cong A C A' C' /\ Cong B C B' C' /\ CongA A C B A' C' B'.
proof: Proof. intros. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B') by (unfold CongA in *;intuition). spliter. assert(exists C'', Out B' C'' C' /\ Cong B' C'' B C). apply l6_11_existence;auto. ex_and H7 C''. assert(B' <> C'') by (unfold Out in *;intuition). assert(~ Col A' B' C') by (eapply ncol_conga_ncol;eauto). 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. assert (C''<> B') by auto. repeat split;try assumption. left. apply between_trivial. left. apply between_trivial. left. apply between_trivial. auto. unfold Out in H7. spliter. assumption. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assert(Cong_3 B A C B' A' C''). repeat split. apply cong_commutativity. assumption. apply cong_symmetry. assumption. assumption. assert(CongA B A C B' A' C''). apply cong3_conga. auto. apply not_col_distincts in H. spliter. auto. assumption. assert(CongA B' A' C' B' A' C''). eapply conga_trans. apply conga_sym. apply H0. assumption. assert(C' = C''). apply conga_os__out in H20. eapply l6_21. apply not_col_permutation_5. apply H10. apply H9. apply col_trivial_2. apply out_col. assumption. apply out_col in H7. assumption. apply col_trivial_2. apply out_one_side. left. intro. apply H10. apply col_permutation_4. assumption. apply l6_6. assumption. subst C''. clear H20. split. assumption. split. eapply cong2_conga_cong. apply H19. apply cong_commutativity. assumption. assumption. apply cong3_conga. apply not_col_distincts in H. spliter. assumption. auto. unfold Cong_3. repeat split. assumption. assumption. apply cong_symmetry. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2