proposition: Lemma mid_onc__diam : forall O P A B, OnCircle A O P -> Midpoint O A B -> Diam A B O P.
proof: Proof. intros O P A B HA HB. repeat split; Between. apply (symmetric_oncircle A); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel