proposition: Lemma midpoint_col : forall A M B, Midpoint M A B -> Col M A B.
proof: Proof. intros. unfold Col. right;right. apply midpoint_bet. apply l7_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR