proposition: Lemma circle_circle__circle_circle_two : circle_circle <-> circle_circle_two.
proof: Proof. unfold circle_circle, circle_circle_two. split. { intros Hcc A B C D P Q. intros. destruct (eq_dec_points A C). subst C. exists P; exists P. assert (Cong A B A D). apply le_anti_symmetry. apply (l5_6 A B A Q); Cong. apply (l5_6 A P A B); Cong. assert (Cong A P A B) by (apply cong_transitivity with A D; Cong). repeat split; trivial. intro Habs. destruct Habs. contradiction. destruct (Hcc A B C D P Q) as [Z1 [HZ1A HZ1B]]; trivial. exists Z1. destruct (l10_6_existence A C Z1) as [Z2 HZ2]. exists Z2. assert (Cong Z1 C Z2 C) by (apply (is_image_col_cong A C Z1 Z2 C); Col). assert (Cong Z1 A Z2 A) by (apply (is_image_col_cong A C Z1 Z2 A); Col). repeat split; trivial; [CongR..|]. intros. intro; subst Z2. clean. destruct (or_bet_out A C Z1) as [HBet|[HOut|HNCol]]. - apply (lt__nle A B A Q); trivial. apply l5_6 with A Q A Z1; Cong. apply triangle_inequality with C; trivial. apply cong_transitivity with C D; Cong. - apply (lt__nle A P A B); trivial. apply l5_6 with A Z1 A P; Cong. apply triangle_reverse_inequality with C; trivial. apply cong_transitivity with C D; Cong. - assert (HCol := l10_8 A C Z1 HZ2); Col. } intros Hcct A B C D P Q. intros. destruct (Hcct A B C D P Q) as [Z1 [Z2 [HZ1On [HZ1On' _]]]]; trivial. exists Z1; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv