proposition: Lemma center_onc2_mid__ncol : forall O P A B M , O <> P -> ~ Col O A B -> OnCircle A O P -> OnCircle B O P -> Midpoint M A B -> ~ Col A O M.
proof: Proof. intros. intro. assert_diffs. unfold Midpoint in H3. spliter. apply H0. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel