proposition: Lemma fod__circle_circle : first_order_dedekind -> circle_circle.
proof: Proof. intro dedekind. apply circle_circle_aux. intros A B C D P Q HPOn HQOn HPIn HQOut HDij. 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 (P <> Q) by (intro; apply (not_and_lt A P A B); subst; split; trivial). assert (C <> D) by (intro; treat_equalities; auto). assert (HOS : forall X Y, Bet P X Q -> Bet P Y Q -> X <> P -> X <> Q -> Y <> P -> Y <> Q -> OS A C X Y). { intros X Y; intros. destruct HDij as [HOS|[[HP HQ]|[HQ HP]]]. - apply one_side_transitivity with P; [apply one_side_symmetry|]; apply l9_17 with Q; trivial. - apply one_side_transitivity with Q; [apply one_side_symmetry|]; apply out_one_side_1 with P; Col; apply l6_6, bet_out; auto. - apply one_side_transitivity with P; [apply one_side_symmetry|]; apply out_one_side_1 with Q; Col; apply l6_6, bet_out; Between. } assert (HNTS : forall X Y, Bet P Y Q -> Bet P X Y -> ~ TS A C X Y). { intros X Y HX HY HTS. absurd (TS A C P Q). - destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]]; [apply l9_9_bis; trivial|intro..]. apply (two_sides_not_col A C P Q); Col. apply (two_sides_not_col A C Q P); Col; Side. - apply bet_ts__ts with Y; trivial. apply l9_2, bet_ts__ts with X; Side; Between. } assert (HLta : LtA A C P A C Q). { apply t18_19; Cong. intro; treat_equalities; auto. apply cong_transitivity with C D; Cong. apply lt_comm, lt_transitivity with A B; trivial. } assert (HNCol1 : ~ Col P Q C). { intro. destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]]; [|apply HNCol; ColR..]. destruct HLta as [_ HNCongA]. apply HNCongA, out2__conga. apply out_trivial; auto. apply col_one_side_out with A; Col; Side. } assert (Haux : forall X Y X0 Y0, Bet P Y Q -> X <> Y -> OnCircle X0 C D -> Out C X X0 -> OnCircle Y0 C D -> Out C Y Y0 -> Bet P X Y -> Lt A X0 A Y0). { intros X Y X0 Y0; intros. apply t18_18 with C C; Cong. apply cong_transitivity with C D; Cong. apply lta_comm, (conga_preserves_lta A C X A C Y). apply out2__conga; [apply out_trivial|apply l6_6]; auto. apply out2__conga; [apply out_trivial|apply l6_6]; auto. split. { apply inangle__lea. assert_diffs. apply l11_24, in_angle_trans with P. repeat split; auto; exists X; split; Between; right; apply out_trivial; auto. apply in_angle_trans2 with Q. repeat split; auto. exists Y; split; Between. right; apply out_trivial; auto. destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]]. - apply l11_24, lea_in_angle; [Lea|Side]. - apply out341__inangle; auto. apply not_bet_out; Col. intro; apply (lta__nlea A C P A C Q); Lea. - apply in_angle_line; auto. apply between_symmetry, not_out_bet; Col. intro; apply (lta__nlea A C P A C Q); trivial. apply l11_31_1; auto. } intro. destruct (conga_cop__or_out_ts A C X Y); trivial. - assert (Col P Q X) by ColR. apply coplanar_pseudo_trans with P Q C; [assumption| |Cop..]. destruct HDij as [|[[]|[]]]; Cop. - absurd (X = Y); trivial; assert_diffs; apply (l6_21 P Q C X); ColR. - apply (HNTS X Y); trivial. } assert (HR : exists R, forall X Y, (Bet P X Q /\ (exists X0, OnCircle X0 C D /\ Out C X X0 /\ InCircle X0 A B)) -> (Bet P Y Q /\ (exists Y0, OnCircle Y0 C D /\ Out C Y Y0 /\ OutCircle Y0 A B)) -> Bet X R Y). { apply dedekind; [repeat constructor..|]. exists P. intros X Y [HX [X0]] [HY [Y0]]. destruct (l5_3 P X Y Q); trivial. destruct (eq_dec_points X Y). subst; Between. exfalso. spliter. apply (lt__nle A Y0 A X0). apply (Haux Y X); auto. apply le_transitivity with A B; trivial. } assert (HP : exists X0, OnCircle X0 C D /\ Out C P X0 /\ InCircle X0 A B). exists P; repeat (split; Circle); apply out_trivial; assert_diffs; auto. assert (HQ : exists Y0, OnCircle Y0 C D /\ Out C Q Y0 /\ OutCircle Y0 A B). exists Q; repeat (split; Circle); apply out_trivial; assert_diffs; auto. destruct HR as [R HR]. assert (HBet : Bet P R Q) by (apply HR; split; Between). assert (R <> C) by (intro; subst; apply HNCol1; Col). destruct (onc_exists C D R) as [Z [HZ1 HZ2]]; auto. exists Z; split; trivial. assert (A <> B) by (apply (lt_diff A P), HPIn). destruct (circle_cases A B Z) as [|[Habs|Habs]]; trivial; exfalso. - assert (Q <> R). { intro; subst R. assert (Q = Z) by (apply (inc_onc2_out__eq C D C); Circle). subst. apply outcs__ninc in HQOut; Circle. } assert (HNCol2 : ~ Col C Q R) by (intro; apply HNCol1; ColR). assert (HT : exists T, OnCircle T A B /\ Bet A Z T). { destruct (eq_dec_points Z A). subst; exists B; split; Circle; Between. destruct (onc_exists A B Z) as [T [HT1 HT2]]; auto. exists T; split; trivial. apply l6_13_1; trivial. apply (l5_6 A Z A B); Cong; Le. } destruct HT as [T [HT1 HT2]]. assert (T <> Z). intro; subst; apply incs__noutc in Habs; apply Habs; Circle. destruct (ex_per_cong C R Z Q T Z) as [I [HI1 [HI2 HI3]]]; Col. assert_diffs. assert (HNCol3 : ~ Col I Z C) by (apply per_not_col; auto). destruct (onc_exists C D I) as [X0 [HX0On HX0Out]]; auto. assert (HLt : Lt C X0 C I). { destruct (l11_46 I Z C) as [_ HLt]; auto. apply (cong2_lt__lt Z C I C); trivial. apply cong_transitivity with C D; Cong. Cong. } assert (X0 <> I) by (intro; apply (nlt C I); subst; assumption). assert (HNCol4 : ~ Col I X0 Z) by (intro; apply (one_side_not_col123 C R I Q); ColR). assert (HLt1 : Lt X0 Z I Z). { assert_diffs. destruct (l11_46 I X0 Z); auto. right. apply acute_bet__obtuse with C; auto. apply l6_13_1; [apply l6_6|]; Le. assert_diffs; apply cong__acute; auto. apply cong_transitivity with C D; Cong. } assert (HX0In : InCircleS X0 A B). { destruct (le_bet Z T Z X0) as [M [HM1 HM2]]. apply (l5_6 X0 Z I Z); Cong; Le. assert (HMT : M <> T). { intro. apply (nlt Z M). apply (cong2_lt__lt X0 Z I Z); trivial; [|subst M; apply cong_transitivity with T Z]; Cong. } apply le1234_lt__lt with A M. - apply triangle_inequality with Z; Cong; eBetween. - apply (cong2_lt__lt A M A T); Cong. assert (Bet A M T) by eBetween. split; Le. intro. apply HMT, (between_cong A); assumption. } assert_diffs. assert (HX : InAngle X0 R C Q). { apply l11_25 with X0 Z Q; try (apply out_trivial); auto. apply lea_in_angle. - apply t18_19; auto. apply cong_transitivity with C D; Cong. Cong. apply le3456_lt__lt with I Z; trivial. apply (l5_6 T Z Q Z); Cong. assert (HLe : Le A T A Q) by (apply (l5_6 A B A Q); Cong; Le). destruct (eq_dec_points A Z). subst; Le. destruct (l5_5_1 A T A Q) as [M [HM1 HM2]]; trivial. assert (Bet A Z M) by eBetween. apply le_transitivity with M Z. apply bet__le2313; eBetween. apply le_comm, (triangle_reverse_inequality A); Cong. apply bet_out; auto. - apply invert_one_side, col_one_side with R; Col. apply one_side_transitivity with I; Side. apply out_one_side; trivial. left; apply one_side_not_col123 with Q; trivial. } destruct HX as [_ [_ [_ [X [HX1 [HX2|HX2]]]]]]. subst; apply HNCol2; Col. assert (X = R). apply between_equality with Q; trivial. apply HR; split; [eBetween|..]; Between. exists X0; repeat (split; Circle). subst; apply HNCol4; ColR. - assert (P <> R). { intro; subst R. assert (P = Z) by (apply (inc_onc2_out__eq C D C); Circle). subst. apply incs__noutc in HPIn; Circle. } assert (HNCol2 : ~ Col C P R) by (intro; apply HNCol1; ColR). destruct (onc_exists A B Z) as [T [HT1 HT2]]; auto. apply (lt_diff A B), lt_right_comm, Habs. assert (HT3 : Bet A T Z). { apply l6_13_1. apply l6_6, HT2. apply (l5_6 A B A Z); Cong; Le. } assert (T <> Z). intro; subst; apply outcs__ninc in Habs; apply Habs; Circle. destruct (ex_per_cong C R Z P T Z) as [I [HI1 [HI2 HI3]]]; Col. assert_diffs. assert (HNCol3 : ~ Col I Z C) by (apply per_not_col; auto). destruct (onc_exists C D I) as [Y0 [HY0On HY0Out]]; auto. assert (HLt : Lt C Y0 C I). { destruct (l11_46 I Z C) as [_ HLt]; auto. apply (cong2_lt__lt Z C I C); trivial. apply cong_transitivity with C D; Cong. Cong. } assert (Y0 <> I) by (intro; apply (nlt C I); subst; assumption). assert (HNCol4 : ~ Col I Y0 Z) by (intro; apply (one_side_not_col123 C R I P); ColR). assert (HLt1 : Lt Y0 Z I Z). { assert_diffs. destruct (l11_46 I Y0 Z); auto. right. apply acute_bet__obtuse with C; auto. apply l6_13_1; [apply l6_6|]; Le. assert_diffs; apply cong__acute; auto. apply cong_transitivity with C D; Cong. } assert (HY0OutC : OutCircleS Y0 A B). { destruct (le_bet Z T Z Y0) as [M [HM1 HM2]]. apply (l5_6 Y0 Z I Z); Cong; Le. assert (HTM : T <> M). { intro. apply (nlt Z M). apply (cong2_lt__lt Y0 Z I Z); trivial; [|subst M; apply cong_transitivity with T Z]; Cong. } apply le3456_lt__lt with A M. - apply (cong2_lt__lt A T A M); Cong. assert (Bet A T M) by eBetween. split; Le. intro. apply HTM, (between_cong A); assumption. - apply (triangle_reverse_inequality Z); Cong. assert_diffs; apply l6_6, bet_out; eBetween. } assert_diffs. assert (HY : InAngle Y0 P C R). { apply l11_25 with Y0 P Z; try (apply out_trivial); auto. apply l11_24, lea_in_angle. - apply t18_19; auto. apply cong_transitivity with C D; Cong. Cong. apply le3456_lt__lt with I Z; trivial. apply (l5_6 T Z P Z); Cong. destruct (le_bet A T A P) as [M [HM1 HM2]]. apply (l5_6 A P A B); Cong; Le. assert (Bet A M Z) by eBetween. destruct (eq_dec_points M A). treat_equalities; Le. apply le_transitivity with M Z. apply bet__le2313; eBetween. apply le_comm, (triangle_reverse_inequality A); Cong. apply l6_6, bet_out; auto. - apply invert_one_side, col_one_side with R; Col. apply one_side_transitivity with I; Side. apply out_one_side; trivial. left; apply one_side_not_col123 with P; trivial. } destruct HY as [_ [_ [_ [Y [HY1 [HY2|HY2]]]]]]. subst; apply HNCol2; Col. assert (Y = R). apply between_equality with P; apply between_symmetry; trivial. apply HR; split; [Between..| |]; [eBetween|]. exists Y0; repeat (split; Circle). subst; apply HNCol4; ColR. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles