proposition: Lemma circle_circle' : circle_circle -> forall C D F G J K P Q R S, CI J C R S -> InCirc P J -> OutCirc Q J -> CI K D F G -> OnCirc P K -> OnCirc Q K -> exists X, OnCirc X J /\ OnCirc X K.
proof: Proof. intros. unfold circle_circle in H. destruct J. destruct p. destruct K. destruct p. unfold CI in *. spliter. injection H0;intros;subst. injection H3;intros;subst. clear H0 H3. unfold OnCirc in *. unfold InCirc in *. destruct H1 as [D1 [D2 HD]]. spliter. unfold OutCirc in *. destruct H2 as [X HX]. spliter. assert (OnCircle P D Q) by CongR. assert (OnCircle Q D Q) by CongR. assert (InCircle P C D1). { unfold InCircle. destruct (eq_dec_points C P). subst. apply le_trivial. assert (TwoCases:Definitions.BetS D1 P C \/ Definitions.BetS C P D2) by (apply bet_cases;auto). destruct TwoCases. exists P. split; Cong; unfold Definitions.BetS in *;spliter; Between. apply l5_6 with C P C D2. exists P. split; Cong; unfold Definitions.BetS in *;spliter; auto. Cong. apply cong_transitivity with R S; Cong. } assert (OutCircle Q C D1). { unfold OutCircle. exists X. split; [unfold Definitions.BetS in *;spliter; auto|CongR]. } assert (Hex: exists Z : Tpoint, OnCircle Z C D1 /\ OnCircle Z D Q) by eauto. destruct Hex as [Z []]. exists Z. split; CongR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates