proposition: Lemma l11_22b : forall A B C P A' B' C' P', OS B P A C /\ OS 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. prolong A B D A B. prolong A' B' D' A' B'. assert(CongA D B P D' B' P'). eapply l11_13. apply H1. assumption. intro. subst D. apply cong_symmetry in H4. apply cong_identity in H4. subst A. unfold CongA in H1. spliter. absurde. assumption. intro. subst D'. apply cong_symmetry in H6. apply cong_identity in H6. subst A'. unfold CongA in H1. spliter. absurde. assert (CongA D B C D' B' C'). eapply (l11_22a _ _ _ P _ _ _ P'). split. eapply l9_2. eapply l9_8_2; [|apply H]. unfold OS in H. ex_and H T. unfold TS in H. unfold TS in H8. spliter. repeat split. assumption. intro. apply H. apply col_permutation_2. eapply (col_transitivity_1 _ D). intro. subst D. unfold CongA in H7. spliter. absurde. apply col_permutation_4. assumption. unfold Col. right; right. assumption. exists B. split. apply col_trivial_1. assumption. split. eapply l9_2. eapply l9_8_2; [|apply H0]. unfold OS in H0. ex_and H0 T'. unfold TS in H0. unfold TS in H8. spliter. repeat split. assumption. intro. apply H0. apply col_permutation_2. eapply (col_transitivity_1 _ D'). intro. subst D'. unfold CongA in H7. spliter. absurde. apply col_permutation_4. assumption. unfold Col. right; right. assumption. exists B'. split. apply col_trivial_1. assumption. split; assumption. eapply l11_13. apply H8. apply between_symmetry. assumption. intro. subst A. unfold CongA in H1. spliter. absurde. apply between_symmetry. assumption. intro. subst A'. unfold CongA in H1. spliter. absurde. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2