proposition: Lemma bet_out_out_bet : forall A B C A' C', Bet A B C -> Out B A A' -> Out B C C' -> Bet A' B C'.
proof: Proof. intros. unfold Out in *. spliter. induction H5; induction H3. assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between). apply outer_transitivity_between with C; auto. assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between). apply between_inner_transitivity with C; assumption. assert(Bet A' B C) by (apply between_exchange3 with A; Between). apply outer_transitivity_between with C; auto. assert(Bet A' B C) by (apply between_exchange3 with A; Between). eapply between_inner_transitivity with C; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le