proposition: Lemma col_out2_col : forall A B C AA CC, Col A B C -> Out B A AA -> Out B C CC -> Col AA B CC.
proof: Proof. intros. induction H. assert (Bet AA B CC). eapply bet_out_out_bet. apply H. assumption. assumption. unfold Col. left. assumption. induction H. assert(Out B AA CC). eapply l6_7. eapply l6_6. apply H0. apply l6_6. eapply l6_7. apply l6_6. apply H1. apply bet_out. unfold Out in *. spliter. assumption. unfold Out in *. spliter. assumption. apply col_permutation_4. apply out_col. assumption. assert(Out B AA CC). eapply l6_6. eapply l6_7. eapply l6_6. apply H1. eapply l6_6. eapply l6_7. eapply l6_6. apply H0. apply bet_out. unfold Out in *. spliter. assumption. unfold Out in *. spliter. apply between_symmetry. assumption. apply col_permutation_4. apply out_col. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le