feat(algebra/floor): Floor and ceil of `-a` (#9715)
This proves `floor_neg : ⌊-a⌋ = -⌈a⌉` and `ceil_neg : ⌈-a⌉ = -⌊a⌋` and uses them to remove explicit dependency on the definition of `int.ceil` in prevision of #9591. This also proves `⌊a + 1⌋ = ⌊a⌋ + 1` and variants.
