proposition: Lemma midpoint_distinct : forall A B X C C', ~ Col A B C -> Col A B X -> Midpoint X C C' -> C <> C'.
proof: Proof. intros. intro. subst C'. apply H. unfold Midpoint in H1. spliter. treat_equalities. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR