transformation `compute` is too permissive with respect to division
With the file
use int.Int
use int.ComputerDivision
goal g : div 1 0 = 0
the transformation compute_in_goal
solves the goal, which is incorrect.
Probably the same mistake with rem
, and with EuclideanDivision
too.