proposition: Lemma similitude_conserve_contact_cercle_cercle : forall (I A A' B B' K K' O O' : PO) (k a : R), k > 0 -> O <> A -> K <> B -> A' = similitude I k a A -> B' = similitude I k a B -> K' = similitude I k a K -> O' = similitude I k a 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 cercles_tangents_tangente_commune; try exact H11 ] ] ] | auto | auto | auto ]. elim existence_similitude_Ika with (I := I) (M := T) (k := k) (a := a); [ intros T' H13; try clear existence_similitude_Ika; try exact H13 | auto ]. elim existence_similitude_Ika with (I := I) (M := M) (k := k) (a := a); [ intros M' H14; try clear existence_similitude_Ika; try exact H14 | auto ]. assert (distance O' A' = k * distance O A). rewrite <- (distance_similitude (k:=k) (a:=a) (I:=I) (A:=O) (B:=A) (A':=O') (B':=A')) ; auto with geo. assert (distance K' B' = k * distance K B). rewrite <- (distance_similitude (k:=k) (a:=a) (I:=I) (A:=K) (B:=B) (A':=K') (B':=B')) ; auto with geo. assert (distance T' M' = k * distance T M). rewrite <- (distance_similitude (k:=k) (a:=a) (I:=I) (A:=T) (B:=M) (A':=T') (B':=M')) ; auto with geo. assert (k <> 0); auto with real. assert (O' <> A'). apply produit_distance_distinct with (3 := H15); auto. assert (K' <> B'). apply produit_distance_distinct with (3 := H16); auto. assert (T' <> M'). apply produit_distance_distinct with (3 := H17); auto. apply tangente_commune_cercles_tangents with (B := T') (M := M'); auto. apply similitude_conserve_contact_cercle_droite with (2 := H2) (6 := H11); auto with geo. apply similitude_conserve_contact_cercle_droite with (2 := H3) (6 := H12); auto with geo. Qed.