evaluate int.floor and int.fract with norm_num

[vihdzp]

Currently, norm_num can only solve goals of the form int.fract x = x, which it does accidentally by simping it to 0 ≤ x ∧ x < 1.

[linesthatinterlace]

Just trying to understand what you want here. You want goals of the form int.floor x = y to reduce to something like y ≤ x ∧ x < y.succ (for x in a floor_ring and y in int)? I'm not sure what you envisage with int.fract though.

[digama0]

The idea is that int.floor and int.fract should compute on rational numerals, for example int.floor (5 / 2) = 2 and int.fract (5 / 2) = 1 / 2.