Mechanizing some advanced refinement concepts
scientific article; zbMATH DE number 469139