• Glen Mével's avatar
    big_op: weaken all Absorbing conditions using TCOr and Affine · 5e346fc5
    Glen Mével authored
    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 change is spreading the use of the
    `TCOr (Affine _) (Absorbing _)` pattern.