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.

The change should not affect end-users by default.