proposition: Lemma circle_circle_bis__euclid_22 : circle_circle_bis -> euclid_s_prop_1_22.
proof: Proof. intros Hcc A B C D E F A' B' C' D' E' F' HSum1 HSum2 HSum3 HLe1 HLe2 HLe3. exists A, B. destruct (eq_dec_points A B); [|destruct (eq_dec_points C D)]; [| |destruct (eq_dec_points E F)]. - destruct (segment_construction_0 C D A) as [P HCong]. exists P; repeat split; Cong. subst B. apply cong_transitivity with C D; trivial. apply le_anti_symmetry. apply (l5_6 C D C' D'); Cong; apply (sums2__cong56 A A E F); Sums. apply (l5_6 E F E' F'); Cong; apply (sums2__cong56 A A C D); Sums. - exists A; treat_equalities; repeat split; Cong. apply le_anti_symmetry. apply (l5_6 A B A' B'); Cong; apply (sums2__cong56 C C E F); Sums. apply (l5_6 E F E' F'); Cong; apply (sums2__cong56 A B C C); Sums. - exists B; treat_equalities; repeat split; Cong. apply le_anti_symmetry. apply (l5_6 A B A' B'); Cong; apply (sums2__cong56 C D E E); Sums. apply (l5_6 C D C' D'); Cong; apply (sums2__cong56 A B E E); Sums. - destruct (segment_construction_3 A B C D) as [C1 [HC1 HC1']]; auto. destruct (segment_construction_3 B A E F) as [E1 [HE1 HE1']]; auto. destruct (segment_construction B A C D) as [C2 [HC2 HC2']]. destruct (segment_construction A B E F) as [E2 [HE2 HE2']]. assert (Bet C1 E1 C2) by (apply (euclid_22_aux A B C D E F A' B' E' F'); trivial). assert (Bet E1 C1 E2) by (apply (euclid_22_aux B A E F C D B' A' C' D'); Sums; Le). destruct (Hcc A C1 B E1 E1 C1) as [Z [HZ1 HZ2]]; Circle. apply bet_inc2__inc with C1 C2; Circle; apply onc__inc, cong_transitivity with C D; Cong. apply bet_inc2__inc with E1 E2; Circle; apply onc__inc, cong_transitivity with E F; Cong. exists Z; repeat split; Cong. apply cong_transitivity with A C1; Cong. apply cong_transitivity with B E1; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv