proposition: Lemma l11_22_bet : forall A B C P A' B' C' P', Bet A B C -> TS P' B' A' C' -> CongA A B P A' B' P' /\ CongA P B C P' B' C' -> Bet A' B' C'.
proof: Proof. intros. spliter. prolong A' B' C'' B C. assert(CongA C B P C'' B' P'). eapply l11_13. apply H1. assumption. unfold CongA in H2. spliter. assumption. assumption. intro. subst C''. apply cong_symmetry in H4. apply cong_identity in H4. subst C. unfold CongA in H2. spliter. absurde. assert (CongA C'' B' P' C' B' P'). eapply conga_trans. apply conga_sym. apply H5. apply conga_comm. assumption. assert(Out B' C' C'' \/ TS P' B' C' C''). apply conga_cop__or_out_ts. apply coplanar_perm_2, col_cop__cop with A'; Col; Cop. apply ts_distincts in H0. spliter. auto. apply conga_comm. apply conga_sym. assumption. induction H7. unfold Out in H7. spliter. induction H9. eapply between_inner_transitivity. apply H3. assumption. eapply outer_transitivity_between. apply H3. assumption. auto. induction (col_dec C' B' P'). unfold TS in H7. spliter. apply False_ind. apply H7. apply col_permutation_5. assumption. assert (B' <> P'). intro. subst P'. apply H8. apply col_trivial_2. assert (TS B' P' A' C''). unfold TS. repeat split. unfold TS in H0. spliter. intro. apply H0. apply col_permutation_5. assumption. intro. unfold TS in H7. spliter. apply H11. apply col_permutation_5. assumption. exists B'. split. apply col_trivial_1. assumption. assert (OS B' P' C' C''). eapply l9_8_1. apply l9_2. apply invert_two_sides. apply H0. apply l9_2. assumption. apply l9_9_bis in H11. apply invert_two_sides in H7. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2