proposition: Lemma diam__midpoint: forall O P A B, Diam A B O P -> Midpoint O A B.
proof: Proof. intros. unfold Diam in *. spliter. unfold Midpoint. unfold OnCircle in *. split. assumption. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel