proposition: Lemma outcs_exists1 : forall O P X, X <> O -> exists Q, Out O X Q /\ OutCircleS Q O P.
proof: Proof. intros O P X HOX. destruct (segment_construction O X O P) as [Q [HQ1 HQ2]]. exists Q; split. apply bet_out; auto. split. - apply le_comm. exists X. split; Between; Cong. - intro. apply HOX. apply between_cong with Q; Between. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel