proposition: Lemma out_to_bet : forall A B C A' B' C', Col A' B' C' -> (Out B A C <-> Out B' A' C') -> Bet A B C -> Bet A' B' C'.
proof: Proof. intros. induction(out_dec B A C). unfold Out in H2. spliter. induction H4. assert( A = B). eapply between_equality. apply H1. assumption. contradiction. assert(C = B). apply(between_symmetry) in H4. eapply between_equality. apply between_symmetry. apply H1. apply between_symmetry. assumption. contradiction. destruct H0. assert (~Out B' A' C'). intro. apply H2. apply H3. assumption. apply not_out_bet. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le