proposition: Lemma translation_conserve_contact_cercle_cercle : forall I J A A' B B' K K' O O' : PO, O <> A -> K <> B -> A' = translation I J A -> B' = translation I J B -> K' = translation I J K -> O' = translation I J 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_representant_vecteur with (A := T) (B := I) (C := J); [ intros T' H6; try clear existence_representant_vecteur; try exact H6 ]. elim existence_representant_vecteur with (A := M) (B := I) (C := J); [ intros M' H7; try clear existence_representant_vecteur; try exact H7 ]. assert (distance O' A' = distance O A). rewrite <- (translation_isometrie (A:=I) (A':=J) (B:=O) (B':=O') (C:=A) (C':=A')) ; auto with geo. assert (distance K' B' = distance K B). rewrite <- (translation_isometrie (A:=I) (A':=J) (B:=K) (B':=K') (C:=B) (C':=B')) ; auto with geo. assert (O' <> A'). apply (isometrie_distinct (A:=O) (B:=A) (A':=O') (B':=A')); auto. assert (K' <> B'). apply (isometrie_distinct (A:=K) (B:=B) (A':=K') (B':=B')); auto. assert (distance T' M' = distance T M). rewrite <- (translation_isometrie (A:=I) (A':=J) (B:=T) (B':=T') (C:=M) (C':=M')) ; auto with geo. assert (T' <> M'). apply (isometrie_distinct (A:=T) (B:=M) (A':=T') (B':=M')); auto. apply tangente_commune_cercles_tangents with (B := T') (M := M'); auto. apply translation_conserve_contact_cercle_droite with (1 := H1) (5 := H10); auto with geo. apply translation_conserve_contact_cercle_droite with (1 := H2) (5 := H11); auto with geo. Qed.