proposition: Lemma circle_circle_aux : (forall A B C D P Q, OnCircle P C D -> OnCircle Q C D -> InCircleS P A B -> OutCircleS Q A B -> OS A C P Q \/ (Col P A C /\ ~ Col Q A C) \/ (~ Col P A C /\ Col Q A C ) -> exists Z : Tpoint, OnCircle Z A B /\ OnCircle Z C D) -> circle_circle.
proof: Proof. intro Haux. cut (forall A B C D P Q, OnCircle P C D -> OnCircle Q C D -> InCircleS P A B -> OutCircleS Q A B -> Coplanar A C P Q -> (~ Col P A C \/ ~ Col Q A C) -> exists Z : Tpoint, OnCircle Z A B /\ OnCircle Z C D). - intros Haux' A B C D P Q HPOn HQOn HPIn HQOut. assert (HQ' : exists Q', OnCircle Q' C D /\ OutCircle Q' A B /\ Col Q' A C). { destruct (segment_construction A C C D) as [Q' []]. exists Q'. repeat split; Col. apply le_transitivity with A Q; trivial. apply triangle_inequality with C; trivial. apply cong_transitivity with C D; Cong. } clear dependent Q. destruct HQ' as [Q [HQOn [HQOut HCol]]]. destruct (cong_dec A P A B). exists P; split; trivial. destruct (cong_dec A B A Q). exists Q; Circle. assert (HPInS : InCircleS P A B) by (split; trivial). assert (HQOutS : OutCircleS Q A B) by (split; trivial). assert (A <> C). { intro; subst C. apply (not_and_lt A B A P); split; trivial. apply (cong2_lt__lt A B A Q); Cong. apply cong_transitivity with A D; Cong. } assert (C <> D). intro; treat_equalities; apply (not_and_lt A C A B); split; trivial. destruct (col_dec P A C); [|apply Haux' with P Q; Cop]. destruct (exists_cong_per A C C D) as [R [HR1 HR2]]. assert_diffs. apply per_not_col in HR1; auto. destruct (circle_cases A B R) as [HOn|HNOn]. exists R; split; trivial. destruct HNOn; [apply Haux' with R Q|apply Haux' with P R]; Col; Cop. - intros A B C D P Q HPOn HQOn HPIn HQOut HCop HDij. destruct (col_dec P A C) as [HCol|HNCol]. { destruct HDij. contradiction. apply Haux with P Q; auto. } destruct (col_dec Q A C). apply Haux with P Q; auto. destruct (cop__one_or_two_sides A C P Q); trivial; [|apply Haux with P Q; auto]. destruct (l10_2_existence A C P) as [P' HP']. assert_diffs. apply Haux with P' Q; trivial. apply cong_transitivity with C P; trivial. apply cong_commutativity, (is_image_col_cong A C); Col. apply cong2_lt__lt with A P A B; Cong. apply cong_symmetry, cong_commutativity, (is_image_col_cong A C); Col. left. exists P; split; Side. apply l10_14; auto. intro; subst; apply HNCol, l10_8, HP'. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles