divisionInverse' a b = b /= 0 ==> (a `div` b) * b + (a `mod` b) == a

Main> ourCheck divisionInverse'
OK, passed 500 tests.