Definition. cong_equi
cong a b m ↔ divides m (a - b)