proposition: Lemma chords_midpoints_col_par : forall O P A M B C N D, O <> P -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Midpoint M A B -> Midpoint N C D -> Col O M N -> ~ Col O A B -> ~ Col O C D -> Par A B C D.
proof: Proof. intros. assert(Perp O M A B). { apply(mid_onc2__perp O P A B M); Circle. intro. treat_equalities. apply H7. Col. intro. treat_equalities. apply H7; Col. } assert(Perp O N C D). { apply(mid_onc2__perp O P C D N); Circle. intro. treat_equalities. apply H8. Col. intro. treat_equalities. apply H8; Col. } assert(Perp O M C D). { apply (perp_col O N C D M); Col. intro. treat_equalities. apply H7; Col. } apply (l12_9_2D A B C D O M); Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel