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.