proposition: Lemma outcs_exists : forall O P, exists Q, OutCircleS Q O P.
proof: Proof. intros. induction(eq_dec_points O P). subst P. assert(HH:=another_point O). ex_and HH Q. exists Q. unfold OutCircleS. apply lt1123;auto. assert(HH:=segment_construction O P O P). ex_and HH Q. exists Q. split. exists P. split; Cong. intro. assert (P=Q) by eauto using between_cong. treat_equalities;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel