proposition: Lemma rotation_conserve_contact_cercle_cercle : forall (I A A' B B' K K' O O' : PO) (a : R), O <> A -> K <> B -> A' = rotation I a A -> B' = rotation I a B -> K' = rotation I a K -> O' = rotation I 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 H6; elim H6; [ intros M H7; elim H7; [ intros H8 H9; elim H9; [ intros H10 H11; try clear H9 H7 H6; try exact H10 ] ] ] | auto | auto | auto ]. elim existence_rotation_Ia with (I := I) (M := T) (a := a); [ intros T' H6; try clear existence_rotation_Ia; try exact H6 ]. elim existence_rotation_Ia with (I := I) (M := M) (a := a); [ intros M' H7; try clear existence_rotation_Ia; try exact H7 ]. assert (O' <> A'). apply (image_bipoint_distinct (I:=I) (A:=O) (B:=A) (A':=O') (B':=A') (a:=a)); auto. assert (K' <> B'). apply (image_bipoint_distinct (I:=I) (A:=K) (B:=B) (A':=K') (B':=B') (a:=a)); auto. assert (T' <> M'). apply (image_bipoint_distinct (I:=I) (A:=T) (B:=M) (A':=T') (B':=M') (a:=a)); auto. apply tangente_commune_cercles_tangents with (B := T') (M := M'); auto. apply rotation_conserve_contact_cercle_droite with (1 := H1) (5 := H10); auto with geo. apply rotation_conserve_contact_cercle_droite with (1 := H2) (5 := H11); auto with geo. Qed.