feat(algebra/periodic): `fract_periodic` (#15660)
Add the lemma that `int.fract` is periodic with period 1. Note that
this goes in `algebra.periodic` alongside the definition of
`periodic`, rather than `algebra.order.floor` alongside the definition
of `fract`, because of import ordering (`algebra.periodic` ends up
importing `algebra.order.floor`).
