proposition: Lemma circle_circle__circle_circle_bis : circle_circle -> circle_circle_bis.
proof: Proof. intros Hcc A B C D P Q HPOn HPIn HQOn HQIn. destruct (eq_dec_points P Q). subst Q; exists P; split; assumption. destruct (chord_completion C D P Q) as [P' [HP'On HBetQ]]; trivial. destruct (chord_completion A B Q P) as [Q' [HQ'On HBetP]]; trivial. apply (Hcc A B C D P P'); trivial. destruct (le_cases A P' A B); trivial. assert (P' = Q). { apply between_equality with Q'. eBetween. assert_diffs. apply (col_inc_onc2__bet A B); trivial; ColR. } subst. apply cong__le; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv