On utilise les régularités des morphismes de la catégorie cartésienne fermée des espaces cohérents probabilistes pour majorer une distance naturelle sur les (classes d'équivalence observationnelle) de termes de PCF probabilistes par une distance définissable dans le modèle.