proposition: Lemma homothetie_conserve_contact_cercle_cercle : forall (k : R) (I J A A' B B' K K' O O' : PO), O <> A -> K <> B -> k <> 0 -> A' = homothetie k I A -> B' = homothetie k I B -> K' = homothetie k I K -> O' = homothetie k I O -> cercles_tangents O A K B -> cercles_tangents O' A' K' B'.
proof: Proof. intros. elim cercles_tangents_tangente_commune with (O := O) (A := A) (O' := K) (A' := B); [ intros T H7; elim H7; [ intros M H8; elim H8; [ intros H9 H10; elim H10; [ intros H11 H12; try clear H10 H8 H7; try exact H11 ] ] ] | auto | auto | auto ]. elim existence_homothetique with (k := k) (I := I) (A := T); [ intros T' H7 ]. elim existence_homothetique with (k := k) (I := I) (A := M); [ intros M' H8 ]. assert (O' <> A'). apply image_homothetie_distincts with (3 := H5) (4 := H2); auto. assert (K' <> B'). apply image_homothetie_distincts with (3 := H4) (4 := H3); auto. assert (T' <> M'). apply image_homothetie_distincts with (3 := H7) (4 := H8); auto. apply tangente_commune_cercles_tangents with (B := T') (M := M'); auto. apply homothetie_conserve_contact_cercle_droite with (2 := H2) (6 := H11); auto with geo. apply homothetie_conserve_contact_cercle_droite with (2 := H3) (6 := H12); auto with geo. Qed.