chore(algebra/floor): general golf (#9716)
This cleans the file in depth:
* kill some `simp`
* use available dot notation on `≤`
* remove the `by ... ; ...` (there's one left that #9715) takes care of
* group definition and notation of `int.floor`,`int.ceil` and `int.fract`
* move `int.preimage_...` lemmas with the rest of the `ℤ` stuff
* homogeneize variable names
