proposition: Lemma onc_exists : forall O P X, X <> O -> O <> P -> exists Q, OnCircle Q O P /\ Out O X Q.
proof: Proof. intros. assert(HH:=segment_construction_2 X O O P H). ex_and HH Q. exists Q. split. unfold OnCircle. Cong. unfold Out. repeat split; auto. intro. subst Q. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel