proposition: Lemma bet2_out_out : forall A B C B' C', B <> A -> B' <> A -> Out A C C' -> Bet A B C -> Bet A B' C' -> Out A B B'.
proof: Proof. intros. induction(eq_dec_points B' C'). subst C'. unfold Out in *. spliter. repeat split; try assumption. induction H5. left. eapply between_exchange4. apply H2. assumption. eapply l5_3. apply H2. assumption. unfold Out in *. spliter. repeat split. assumption. assumption. induction H6. assert(Bet A B C'). eapply between_exchange4. apply H2. assumption. eapply l5_3. apply H7. assumption. assert(Bet B' C' C). eapply between_exchange3. apply H3. assumption. assert(Bet A B' C). eapply outer_transitivity_between. apply H3. assumption. assumption. eapply l5_3. apply H2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le