Adapt to https://github.com/math-comp/math-comp/pull/1545

[proux01]

Adapt to math-comp/math-comp#1545

This was automatically generated with

for f in $(find . -name "*.v") ; do awk -i inplace -f add_set_reworder.awk $f ; done

where add_set_reworder.awk is the following awk script

BEGIN {
  seen_mc_require= 0
  done= 0
}

/From mathcomp Require/ {
  seen_mc_require= 1
}

/^\r?$/ {
  if (seen_mc_require == 1 && done == 0) {
    print("Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)")
  }
  done= 1
}

{
  print($0)
}

[affeldt-aist]

I would like to start communicating about this change on the occasion of the next release
with a heads-up on Zulip.
What do you think about the following message?

fyi: @strub

Notice to MathComp-Analysis contributors:

This is just a heads-up about a significant change that should happen in
the near future.

We plan to change the default order of subgoals generated by the `rewrite`
tactic as the one implemented by the command `Unset SsrOldRewriteGoalsOrder`.
Indeed, very often when rewriting with a lemma one wants to discharge premises
as soon as possible, resulting in the frequent usage of, e.g., the `; last first`
tactical. `Unset SsrOldRewriteGoalsOrder` fixes this issue by generating premises
as the first subgoals. It is actually already in use in a few places in the source code.

Note that the current settings stem from the core MathComp library
(that does `Set SsrOldRewriteGoalsOrder` in `ssreflect.v`) and that the core
MathComp library will also implement this change.

The change should not affect end-users by default.

[affeldt-aist]

That looks like a good preparatory step to transition to an often better behaved rewrite tactic!

Note that
distr.v
realseq.v
realsum.v
are doing
Unset SsrOldRewriteGoalsOrder.
just after the newly added Set command.

fyi: @strub

[affeldt-aist]

(oh, this was just a draft PR! but anyway if the CI is green, we can think of merging, it is pretty harmless)

[proux01]

No, CI is still red in the upstream PR, I still need to fix it.