big_op: weaken all Absorbing conditions using TCOr and Affine

For all big_op lemmas which had an Absorbing condition, the condition has now become an alternative between Affine and Absorbing. Thus the lemmas are made more general. This is spreading the use of the TCOr (Affine _) (Absorbing _) pattern.

Impact on reverse dependencies needs assessment. As this MR only weakens existing TC arguments, in theory it shouldn’t cause many breakages, but experience shows that TCOr instances are not always inferred fully automatically.