proposition: Lemma bet_col1 : forall A B C D, Bet A B D -> Bet A C D -> Col A B C.
proof: Proof. intros. assert(Bet A B C \/ Bet A C B). eapply l5_3. apply H. assumption. unfold Col. induction H1. left. assumption. right; left. apply between_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR