proposition: Lemma euclid_22__circle_circle : euclid_s_prop_1_22 -> circle_circle.
proof: Proof. intros p22 A B C D P Q HPOn HQOn HPIn HQOut. assert (HXYZ : exists X Y Z : Tpoint, Cong X Y A C /\ Cong X Z A B /\ Cong Y Z C D). { destruct (ex_sums A B C D) as [L1 [R1]]. destruct (ex_sums A C C D) as [L2 [R2]]. destruct (ex_sums A C A B) as [L3 [R3]]. apply p22 with L1 R1 L2 R2 L3 R3; trivial. - destruct (ex_sums C A A P) as [R [S]]. apply le_transitivity with R S. apply (l5_6 C P R S); Cong; apply triangle_inequality1 with A; trivial. apply le2_sums2__le with C A A P A C A B; Le. - apply le_transitivity with A Q; Le. apply (triangle_inequality1 A C Q). apply (cong3_sums__sums A C C D L2 R2); Cong. - destruct (ex_sums A P P C) as [R [S]]. apply le_transitivity with R S. apply triangle_inequality1 with P; trivial. apply le2_sums2__le with A P P C A B C D; Le. } destruct (eq_dec_points A C). { subst C. exists B; split; Circle. apply le_anti_symmetry. apply le_transitivity with A Q; Le. apply le_transitivity with A P; Le. } destruct (eq_dec_points A B). { subst B. exists P; split; trivial. apply inc_eq in HPIn; subst; Circle. } destruct HXYZ as [X [Y [Z [HAC [HAB HCD]]]]]. assert_diffs. assert (HZ0 : exists Z0, CongA Y X Z C A Z0 /\ Cong X Z A Z0). { destruct (angle_construction_3 Y X Z C A) as [Z']; auto. assert_diffs. destruct (segment_construction_3 A Z' X Z) as [Z0 []]; auto. exists Z0; split; Cong. apply l11_10 with Y Z C Z'; [|apply out_trivial..|apply l6_6]; auto. } destruct HZ0 as [Z0 []]. exists Z0. destruct (l11_49 Y X Z C A Z0); trivial. split. apply cong_transitivity with X Z; Cong. apply cong_transitivity with Y Z; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv