Commit 2022-08-09 14:16 eb55b1e9

chore(algebra/order/floor): generalize lemmas about adding nat from rings to semirings (#15952) This generalizes this typeclass argument of the following lemmas:

• nat.floor_add_nat
• nat.floor_add_one
• nat.ceil_add_nat
• nat.ceil_add_one
• nat.floor_sub_nat These generalizations are useful for nnreal and a future nnrat.