proposition: Lemma mid_chord__diam_or_ncol : forall O P A B T, A <> B -> OnCircle A O P -> OnCircle B O P -> Midpoint T A B -> Diam A B O P \/ ~Col O A T /\ ~Col O B T.
proof: Proof. intros. unfold Midpoint in H2. spliter. apply(bet_chord__diam_or_ncol);auto. intro. treat_equalities; tauto. intro. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel