floor): `fract_one` (#15785)

Commit

3 years ago

feat(algebra/order/floor): `fract_one` (#15785) This seems to be an appropriate `simp` lemma, but is currently missing.

Author

jsm28

Parents