proposition: Lemma onc3_mid2__ncol : forall O P A B C A' B', O <> P -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Midpoint A' A C -> Midpoint B' B C -> ~ Col A B C -> ~ Col O A' B' \/ A' = O \/ B' = O.
proof: Proof. intros. induction(col_dec O A C). assert(A = C \/ Midpoint O A C) by (apply l7_20; [Col|CongR]). induction H7. treat_equalities. apply False_ind. apply H5; Col. right; left. apply (l7_17 A C); auto. induction(col_dec O B C). assert(B = C \/ Midpoint O B C) by (apply l7_20; [Col|CongR]). induction H8. treat_equalities. apply False_ind. apply H5; Col. right; right. apply (l7_17 B C); auto. left. intro. assert(HH:=chords_midpoints_col_par O P A A' C B B' C H H0 H2 H1 H2 H3 H4 H8 H6 H7). induction HH. apply H9. exists C. split; Col. spliter; contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel