proposition: Lemma mid_onc2__per : forall O P U V X, OnCircle U O P -> OnCircle V O P -> Midpoint X U V -> Per O X U.
proof: Proof. intros. unfold Per. exists V. unfold OnCircle in *. split; trivial. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel