proposition: Lemma incs_exists1 : forall O P X, X <> O -> P <> O -> exists Q, Out O X Q /\ InCircleS Q O P.
proof: Proof. intros O P X HOX HOP. destruct (midpoint_existence O P) as [M HM]. destruct (segment_construction_3 O X O M) as [Q [HQ1 HQ2]]; auto. intro; treat_equalities; auto. exists Q; split; auto. apply (cong2_lt__lt O M O P); Cong. apply mid__lt; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel