coq 8.20 has a small regression with lia.
+ some small stdlib changes.

By modifying the gathering with no light to break bivalent position at
start if needed.

has the drawback to make rewritting an equivalence between functions
more complex (anon better than pointwise to avoid that?)

Thanks to Proofgeneral which insert them automatically.