proposition: Lemma prop_1_circle_circle : circle_circle -> forall A B, exists C, Cong A B A C /\ Cong A B B C.
proof: Proof. intros cc A B. apply circle_circle__circle_circle_bis in cc. destruct (cc A B B A A B) as [C [HC1 HC2]]; Circle. exists C. split;Cong. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions