proposition: Lemma bet_chord__diam_or_ncol : forall O P A B T, A <> B -> T <> A -> T <> B -> OnCircle A O P -> OnCircle B O P -> Bet A T B -> Diam A B O P \/ ~Col O A T /\ ~Col O B T.
proof: Proof. intros. induction(col_dec O A B). left. apply(center_col__diam); Col. right. split. intro. apply H5; ColR. intro. apply H5; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel