proposition: Lemma onc2_per__mid : forall O P U V M, U <> V -> M <> U -> OnCircle U O P -> OnCircle V O P -> Col M U V -> Per O M U -> Midpoint M U V .
proof: Proof. intros. assert(HH:=midpoint_existence U V). ex_and HH M'. assert(HH:=(mid_onc2__per O P U V M' H1 H2 H5)). assert(M = M' \/ ~ Col M' U V). apply(col_per2_cases O M U V M'); Col. assert_diffs;auto. induction H6. subst M'. assumption. apply False_ind. apply H6. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel