proposition: Lemma cong_col_mid : forall A B C, A <> C -> Col A B C -> Cong A B B C -> Midpoint B A C.
proof: Proof. intros. apply l7_20 in H0. intuition subst. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR