proposition: Lemma translation_conserve_contact_cercle_droite : forall I J A A' B B' M M' O O' : PO, A' = translation I J A -> B' = translation I J B -> M' = translation I J M -> O' = translation I J O -> tangente_cercle O A B M -> tangente_cercle O' A' B' M'.
proof: Proof. icercle. rewrite (translation_isometrie (A:=I) (A':=J) (B:=O) (B':=O') (C:=A) (C':=A')) ; auto. rewrite (translation_isometrie (A:=I) (A':=J) (B:=O) (B':=O') (C:=B) (C':=B')) ; auto. apply (translation_conserve_orthogonalite (I:=I) (J:=J) (A:=B) (A':=B') (B:=M) (B':=M') (M:=O) (M':=O')); auto. Qed.