proposition: Lemma circle_circle_bis__circle_circle_axiom : circle_circle_bis <-> circle_circle_axiom.
proof: Proof. split; intro cc. - intros A B C D B' D' HCong1 HCong2 HBet1 HBet2. apply cc with D' B'; try apply bet__le1213; trivial. - intros A B C D P Q HPOn HPIn HQOn HQIn. assert (HQ' : Le A P A Q) by (apply le_transitivity with A B; Le). apply l5_5_1 in HQ'. destruct HQ' as [Q' [HBet1 HCong1]]. assert (HP' : Le C Q C P) by (apply le_transitivity with C D; Le). apply l5_5_1 in HP'. destruct HP' as [P' [HBet2 HCong2]]. destruct (cc A Q' C P' Q P) as [Z []]; Cong. exists Z; split. apply cong_transitivity with A Q; [apply cong_transitivity with A Q'|]; Cong. apply cong_transitivity with C P; [apply cong_transitivity with C P'|]; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv