proposition: Lemma prop_22 : circle_circle -> forall A1 A2 B1 B2 C1 C2 A1' A2' B1' B2' C1' C2', SumS A1 A2 B1 B2 C1' C2' -> SumS A1 A2 C1 C2 B1' B2' -> SumS B1 B2 C1 C2 A1' A2' -> Le C1 C2 C1' C2' -> Le B1 B2 B1' B2' -> Le A1 A2 A1' A2' -> exists F G K, Cong F G A1 A2 /\ Cong F K B1 B2 /\ Cong G K C1 C2.
proof: Proof. intro cc. apply circle_circle__circle_circle_bis in cc. apply (circle_circle_bis__euclid_22 cc). Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions