Merge branch 'ssrpat-FO-ignore-imparg' into 'master'

Adapt to rocq-prover/rocq#20707

See merge request coquelicot/coquelicot!14

Author: silene

theories/SF_seq.v

@@ -1687,7 +1687,7 @@ Proof.
       rewrite /minus 2?(Riemann_sum_cons _ (x0, y1)) SF_cut_down_h.
       rewrite opp_plus plus_assoc /=.
       apply (f_equal (fun x => plus x _)).
-      rewrite (plus_comm (scal (SF_h ptd - x0) (f y1))) -3!plus_assoc.
+      rewrite (plus_comm (scal (SF_h ptd - x0) (f y1))) -!plus_assoc.
       apply f_equal.
       by rewrite plus_comm -plus_assoc plus_opp_l plus_zero_r.
       by [].