Adapt to Coq PR #18591: better refolding of addn induces "simpl never…

…" now respected

An equality "2%N = (1 + \rank V)%N" was previously leading to "1%N = (\rank V)%N"
after injection but with the PR, it respects "simpl never" and only leads to
"1%N = (0 + \rank V)%N". So, we add a rewrite of addSn and add0n to
recover the previous behavior. This rewrite is additionally made
optional so as to preserve the compatibility.

Another simplification, in PFsection13.v, gives "1 + (c - 2)" which
now needs an extra add1n.

theories/BGsection2.v

@@ -897,7 +897,7 @@ have{sU1} [|V Vmod sumUV dxUV] := mx_Maschke _ _ Umod sU1.
 have [u defU]: exists u : 'rV_2, (u :=: U)%MS.
   by move: (row_base U) (eq_row_base U); rewrite Uscal => u; exists u.
 have{dxUV Uscal} [v defV]: exists v : 'rV_2, (v :=: V)%MS.
-  move/mxdirectP: dxUV; rewrite /= Uscal sumUV mxrank1 => [[Vscal]].
+  move/mxdirectP: dxUV; rewrite /= Uscal sumUV mxrank1 ?addSn ?add0n => [[Vscal]].
   by move: (row_base V) (eq_row_base V); rewrite -Vscal => v; exists v.
 pose B : 'M_(1 + 1) := col_mx u v; have{sumUV} uB: B \in unitmx.
   rewrite -row_full_unit /row_full eqn_leq rank_leq_row {1}addn1.

theories/PFsection13.v

@@ -1282,7 +1282,7 @@ have regCW1: semiregular C W1.
   have [[_ _ /Frobenius_reg_ker regUW1 _] _ _ _] := FTtypeP_facts maxS StypeP.
   by move=> _ y /regUW1 regUx; rewrite setIAC regUx setI1g.
 have{regCW1} dv_2q_c1: q.*2 %| c.-1.
-  rewrite -(subnKC c_gt1) -mul2n Gauss_dvd ?coprime2n ?dvdn2 ?mFT_odd //=.
+  rewrite -(subnKC c_gt1) -mul2n Gauss_dvd ?coprime2n ?dvdn2 ?mFT_odd //= ?add1n.
   rewrite oddB ?mFT_odd -?subSn // subn2 regular_norm_dvd_pred //.
   have /mulG_sub[_ sW1S] := sdprodW defS.
   apply: normsI; first by have [_ []] := StypeP.