Commit 2021-10-16 16:46 99b2d40e

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.