proposition: Lemma diam_exists : forall O P T, exists A, exists B, Diam A B O P /\ Col A B T.
proof: Proof. intros. destruct (diam_points O P T) as [A [B [HBet [HCol [HA HB]]]]]. exists A, B. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel