Merge pull request #84 from proux01/reworder

Port to new rewrite goals order

Author: proux01

theories/cauchyreals.v

@@ -5,7 +5,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype bigop binomial order perm ssralg poly.
 From mathcomp Require Import polydiv ssrnum ssrint rat matrix mxpoly polyXY.
 From mathcomp Require Import bigenough polyorder.
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 (***************************************************************************)
 (* This is a standalone construction of Cauchy reals over an arbitrary     *)
@@ -92,8 +92,8 @@ rewrite ler_wpM2l //.
   by rewrite ?mulr_ge0 ?exprn_ge0 ?ler_maxr ?addr_ge0 ?normr_ge0 // ltrW.
 rewrite (ger0_norm r_ge0) ler_norml opprD.
 rewrite (le_trans _ lx) ?(le_trans ux) // lerD2r.
-  by rewrite ler_normr lexx.
-by rewrite lerNl ler_normr lexx orbT.
+  by rewrite lerNl ler_normr lexx orbT.
+by rewrite ler_normr lexx.
 Qed.
 
 Lemma poly_bound_gt0 p a r : 0 < poly_bound p a r.
@@ -120,7 +120,7 @@ rewrite le0r=> /orP[/eqP->|r_gt0 hx hy].
 rewrite mulrA mulrDr mulr1 ler_wpDl ?mulr_ge0 ?normr_ge0 //=.
   by rewrite exprn_ge0 ?le_max ?mulr_ge0 ?ger0E ?ltW.
 rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA.
-rewrite nderiv_taylor; last exact: mulrC.
+rewrite nderiv_taylor; first exact: mulrC.
 have [->|p_neq0] := eqVneq p 0.
   rewrite size_poly0 big_ord0 horner0 subr0 normr0 mulr_ge0 ?normr_ge0 //.
   by rewrite big_ord0 mulr0 lexx.
@@ -148,9 +148,9 @@ Qed.
 Lemma poly_accr_bound_gt0 p a r : 0 < poly_accr_bound p a r.
 Proof.
 rewrite /poly_accr_bound pmulr_rgt0 //.
-  rewrite ltr_wpDr ?ltr01 //.
-  by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0.
-by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n.
+  by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n.
+rewrite ltr_wpDr ?ltr01 //.
+by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0.
 Qed.
 
 Lemma poly_accr_bound_ge0 p a r : 0 <= poly_accr_bound p a r.
@@ -191,8 +191,8 @@ Proof.
 rewrite /norm_poly2; have [->|p0] := eqVneq p 0.
   by rewrite /map_poly poly_def !(size_poly0, big_ord0).
 rewrite /map_poly size_poly_eq // -size_poly_eq0 size_poly_eq //.
-  by rewrite -lead_coefE size_poly_eq0 lead_coef_eq0.
-by rewrite -!lead_coefE normr_eq0 !lead_coef_eq0.
+  by rewrite -!lead_coefE normr_eq0 !lead_coef_eq0.
+by rewrite -lead_coefE size_poly_eq0 lead_coef_eq0.
 Qed.
 
 End polyXY_order_extra.
@@ -210,9 +210,9 @@ Definition poly_accr_bound2 (p : {poly F}) (a r : F) : F
 Lemma poly_accr_bound2_gt0 p a r : 0 < poly_accr_bound2 p a r.
 Proof.
 rewrite /poly_accr_bound pmulr_rgt0 //.
-  rewrite ltr_wpDr ?ltr01 //.
-  by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0.
-by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n.
+  by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n.
+rewrite ltr_wpDr ?ltr01 //.
+by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0.
 Qed.
 
 Lemma poly_accr_bound2_ge0 p a r : 0 <= poly_accr_bound2 p a r.
@@ -232,17 +232,17 @@ move=> neq_xy hx hy.
 rewrite mulrA mulrDr mulr1 ler_wpDl ?mulr_ge0 ?normr_ge0 //=.
   by rewrite exprn_ge0 ?le_max ?mulr_ge0 ?ger0E ?ltW.
 rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA.
-rewrite nderiv_taylor; last exact: mulrC.
+rewrite nderiv_taylor; first exact: mulrC.
 have [->|p_neq0] := eqVneq p 0.
   by rewrite derivC !horner0 size_poly0 !(big_ord0, subrr, mul0r) normr0 !mulr0.
 rewrite -[size _]prednK ?lt0n ?size_poly_eq0 //.
 rewrite big_ord_recl expr0 mulr1 nderivn0 /= -size_deriv.
 have [->|p'_neq0] := eqVneq p^`() 0.
   by rewrite horner0 size_poly0 !big_ord0 addr0 !(subrr, mul0r) normr0 !mulr0.
 rewrite -[size _]prednK ?lt0n ?size_poly_eq0 // big_ord_recl expr1.
-rewrite addrAC subrr add0r mulrDl mulfK; last by rewrite subr_eq0 eq_sym.
+rewrite addrAC subrr add0r mulrDl mulfK; first by rewrite subr_eq0 eq_sym.
 rewrite nderivn1 addrAC subrr add0r mulr_sumr normrM normfV.
-rewrite ler_pdivrMr ?normr_gt0; last by rewrite subr_eq0 eq_sym.
+rewrite ler_pdivrMr ?normr_gt0; first by rewrite subr_eq0 eq_sym.
 rewrite mulrAC -expr2 mulrC mulr_suml.
 have := le_trans (ler_norm_sum _ _ _); apply.
 rewrite ler_sum // => i _ /=; rewrite /bump /= !add1n.
@@ -921,7 +921,7 @@ exists_big_modulus m F.
   move=> e i j e_gt0 hi hj.
   have /andP[xi_neq0 xj_neq0] : (x i != 0) && (x j != 0).
     by rewrite -!normr_gt0 !(lt_le_trans _ (lbound0_of x_neq0)) ?lbound_gt0.
-  rewrite -(@ltr_pM2r _ `|x i * x j|); last by rewrite normr_gt0 mulf_neq0.
+  rewrite -(@ltr_pM2r _ `|x i * x j|); first by rewrite normr_gt0 mulf_neq0.
   rewrite -normrM !mulrBl mulrA mulVf // mulrCA mulVf // mul1r mulr1.
   apply: lt_le_trans (_ : e * d ^+ 2 <= _).
     by apply: cauchymodP; rewrite // !pmulr_rgt0 ?lbound_gt0.
@@ -1367,7 +1367,7 @@ pose_big_enough i.
   exists i => //; left; split; last first.
     move=> y hy; have := (@poly_accr_bound1P _ p^`() 0 (1 + ubound x) (x i) y).
     rewrite ?subr0 ler_wpDl ?ler01 ?uboundP //.
-    rewrite (le_trans (_ : _ <= r + `|x i|)) ?subr0; last 2 first.
+    rewrite (le_trans (_ : _ <= r + `|x i|)) ?subr0.
     + rewrite (monoRL (addrNK _) (lerD2r _)).
       by rewrite (le_trans (lerB_dist _ _)).
     + by rewrite lerD ?ge_min ?lexx ?uboundP.
@@ -1386,11 +1386,11 @@ pose_big_enough i.
   have := (@poly_accr_bound1P _ p^`() 0 (1 + ubound x) (x i) z).
   have := @poly_accr_bound2P _ p 0 (1 + ubound x) z y; rewrite eq_sym !subr0.
   rewrite neq_yz ?ler01 ?ubound_ge0=> // /(_ isT).
-  rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first.
+  rewrite (le_trans (_ : _ <= r + `|x i|)).
   + rewrite (monoRL (addrNK _) (lerD2r _)).
     by rewrite (le_trans (lerB_dist _ _)).
   + by rewrite lerD ?ge_min ?lexx ?uboundP.
-  rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first.
+  rewrite (le_trans (_ : _ <= r + `|x i|)).
   + rewrite (monoRL (addrNK _) (lerD2r _)).
     by rewrite (le_trans (lerB_dist _ _)).
   + by rewrite lerD ?ge_min ?lexx ?uboundP.
@@ -1472,7 +1472,7 @@ Proof.
 rewrite /poly_bound.
 pose f (q : {poly F}) (k : nat) :=  `|q^`N(j.+1)`_k| * (`|a| + `|r|) ^+ k.
 rewrite lerD //=.
-rewrite (big_ord_widen (sizeY q) (f q.[(z i)%:P])); last first.
+rewrite (big_ord_widen (sizeY q) (f q.[(z i)%:P])).
   rewrite size_nderivn leq_subLR (leq_trans (max_size_evalC _ _)) //.
   by rewrite leq_addl.
 rewrite big_mkcond /= ler_sum // /f => k _.
@@ -1483,7 +1483,7 @@ rewrite !(@big_morph _ _ (fun p => p^`N(j.+1)) 0 +%R);
   do ?[by rewrite raddf0|by move=> x y /=; rewrite raddfD].
 rewrite !coef_sum.
 rewrite (le_trans (ler_norm_sum _ _ _)) //.
-rewrite ger0_norm; last first.
+rewrite ger0_norm.
   rewrite sumr_ge0=> //= l _.
   rewrite coef_nderivn mulrn_wge0 ?natr_ge0 //.
   rewrite -polyC_exp coefMC coef_norm_poly2 mulr_ge0 ?normr_ge0 //.
@@ -1518,7 +1518,7 @@ apply: le_trans (_ : u * vi <= _).
   by rewrite max_size_evalC.
 rewrite ler_wpM2l ?exprn_ge0 ?le_max ?ler01 // lerD //.
 pose f j :=  poly_bound q.[(z i)%:P]^`N(j.+1) a r.
-rewrite (big_ord_widen (sizeY q).-1 f); last first.
+rewrite (big_ord_widen (sizeY q).-1 f).
   rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //.
   by rewrite max_size_evalC.
 rewrite big_mkcond /= ler_sum // /f => k _.
@@ -1596,7 +1596,7 @@ have [||[u v] /= [hu hv] hpq] := @div_annihilant_in_ideal _ p q.
 + by rewrite (@has_root_creal_size_gt1 y).
 apply: eq_crealP; exists_big_modulus m F.
   move=> e i e_gt0 hi /=; rewrite subr0.
-  rewrite (hpq (y i)) mulrCA divff ?mulr1; last first.
+  rewrite (hpq (y i)) mulrCA divff ?mulr1.
     by rewrite -normr_gt0 (lt_le_trans _ (lbound0_of y_neq0)) ?lbound_gt0.
   rewrite split_norm_add // normrM.
     apply: le_lt_trans (_ : (ubound u.[y, x / y_neq0]) * `|p.[x i]| < _).

theories/complex.v

@@ -5,7 +5,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp Require Import choice fintype tuple bigop binomial order ssralg.
 From mathcomp Require Import zmodp poly ssrnum ssrint archimedean rat matrix.
 From mathcomp Require Import mxalgebra mxpoly closed_field polyrcf realalg.
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 (**********************************************************************)
 (*   This files defines the extension R[i] of a real field R,         *)
@@ -341,7 +341,7 @@ rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _).
 rewrite -[_ + locked u]addrA [leLHS]addrC addKr -!lock addrC.
 have [huv|] := ger0P (u + v); last first.
   by move=> /ltW /le_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0.
-rewrite -(@ler_pXn2r _ 2) -?topredE //=; last first.
+rewrite -(@ler_pXn2r _ 2) -?topredE //=.
   by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //.
 rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_wpDr, sqr_ge0) //.
 rewrite -mulrnDl -[in leLHS]mulr_natl !exprMn ler_pM2l ?exprn_gt0 ?ltr0n //.
@@ -670,7 +670,7 @@ congr (_ +i* _); set u := if _ then _ else _.
   by rewrite opprK -mulr2n -[a *+ 2]mulr_natl [_*a]mulrC mulfK.
 rewrite mulrCA -mulrA -mulrDr [sqrtr _ * _]mulrC.
 rewrite -mulr2n -sqrtrM // mulrAC !mulrA ?[_ * (_ - _)]mulrC -subr_sqr.
-rewrite sqr_sqrtr; last first.
+rewrite sqr_sqrtr.
   by rewrite ler_wpDr // exprn_even_ge0.
 rewrite [_^+2 + _]addrC addrK -mulrA -expr2 sqrtrM ?exprn_even_ge0 //.
 rewrite !sqrtr_sqr -(mulr_natr (_ * _)).
@@ -826,7 +826,7 @@ rewrite /skew_vec /= !mxvec_delta !mxE !eqxx /=.
 have /(_ _ _ (_, _) (_, _)) /= eq_mviE :=
   inj_eq (bij_inj (onT_bij (curry_mxvec_bij _ _))).
 rewrite eq_mviE xpair_eqE -!val_eqE /= eq_sym andbb.
-rewrite ltn_eqF // subr0 mulr1 summxE big1.
+rewrite ltn_eqF // subr0 mulr1 summxE big1; last first.
   rewrite [w as X in X *m _]mx11_scalar => ->.
   by rewrite mul_scalar_mx scale0r submx0.
 move=> [i' j'] /= /andP[lt_j'i'].
@@ -841,7 +841,7 @@ Hint Resolve skew_direct_sum : core.
 Lemma rank_skew : \rank skew = (n * n.-1)./2.
 Proof.
 rewrite /skew (mxdirectP _) //= -bin2 -triangular_sum big_mkord.
-rewrite (eq_bigr (fun _ => 1%N)); last first.
+rewrite (eq_bigr (fun _ => 1%N)).
   move=> [i j] /= lt_ij; rewrite genmxE.
   apply/eqP; rewrite eqn_leq rank_leq_row /= lt0n mxrank_eq0.
   rewrite /skew_vec /= !mxvec_delta /= subr_eq0.
@@ -857,8 +857,8 @@ apply: eq_bigr => [] [[|i] Hi] _ /=; first by rewrite big1.
 rewrite (eq_bigl _ _ (fun _ => ltnS _ _)).
 have [n_eq0|n_gt0] := posnP n; first by move: Hi (Hi); rewrite {1}n_eq0.
 rewrite -[n]prednK // big_ord_narrow_leq /=.
-  by rewrite -ltnS prednK // (leq_trans _ Hi).
-by rewrite sum_nat_const card_ord muln1.
+  by rewrite sum_nat_const card_ord muln1.
+by rewrite -ltnS prednK // (leq_trans _ Hi).
 Qed.
 
 Lemma skewP (M : 'rV_(n * n)) :
@@ -891,9 +891,9 @@ rewrite (bigID (fun ij => (ij.2 : 'I__) < (ij.1 : 'I__))%N) /=; congr (_ + _).
   apply: eq_bigr => [] [i j] /= lt_ij.
   by rewrite !linearZ linearB /= ?mxvecK trmx_delta scalerN scalerBr.
 rewrite (bigID (fun ij => (ij.1 : 'I__) == (ij.2 : 'I__))%N) /=.
-rewrite big1 ?add0r; last first.
+rewrite big1 ?add0r.
   by move=> [i j] /= /andP[_ /eqP ->]; rewrite linearZ /= trmx_delta subrr.
-rewrite (@reindex_inj _ _ _ _ (fun ij => (ij.2, ij.1))) /=; last first.
+rewrite (@reindex_inj _ _ _ _ (fun ij => (ij.2, ij.1))) /=.
   by move=> [? ?] [? ?] [] -> ->.
 apply: eq_big => [] [i j] /=; first by rewrite -leqNgt ltn_neqAle andbC.
 by rewrite !linearZ linearB /= ?mxvecK trmx_delta scalerN scalerBr.
@@ -1055,7 +1055,7 @@ have [] // := IHn _ (if d %| \rank Z then W else Z) _ _ [:: f' & sf'].
 move=> v v_neq0 Hv; exists (v *m row_base V).
   by rewrite mul_mx_rowfree_eq0 ?row_base_free.
 move=> g Hg; have [|b] := Hv (restrict V g); first by rewrite -map_cons map_f.
-rewrite eigenspace_restrict //; first by exists b.
+rewrite eigenspace_restrict //; last by exists b.
 by move: Hg; rewrite in_cons => /orP [/eqP -> //|/sf_stabV].
 Qed.
 

theories/mxtens.v

@@ -2,7 +2,7 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp Require Import choice fintype bigop ssralg zmodp matrix.
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/ordered_qelim.v

@@ -5,7 +5,7 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp Require Import choice fintype bigop finset order fingroup.
 From mathcomp Require Import ssralg zmodp poly ssrnum.
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -546,7 +546,7 @@ elim: t r0 m => /=; try do [
   by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1].
 move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}.
 case: to_rterm => t1' r1 /= [def_r ub_t1' ub_r1 <-].
-rewrite size_rcons addnS leqnn -{1}cats1 takel_cat ?def_r; last first.
+rewrite size_rcons addnS leqnn -{1}cats1 takel_cat ?def_r.
   by rewrite -def_r size_take geq_minr.
 elim: r1 m ub_r1 ub_t1' {def_r} => /= [|u r1 IHr1] m => [_|[->]].
   by rewrite addn0 eqxx.
@@ -760,13 +760,13 @@ elim: leq1 eq1 lt1 oc2 => [|t1 leq1 ih] eq1 lt1 [eq2 neq2 lt2 leq2] /=.
 rewrite map_cat /= mem_cat -!map_comp; set f := fun _ => _.
 rewrite -/f in ih; case/orP.
   case/mapP=> [[y1 y2]] yin ye.
-  move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //; last first.
+  move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //.
     by move=> [u1 u2] [v1 v2]; rewrite /f /=; case=> -> ->.
   move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h.
   move=> u; rewrite in_cons (h u) !mem_cat in_cons.
   by rewrite orbC !orbA; set x := _ || (u \in lt1); rewrite orbAC.
 case/mapP=> [[y1 y2]] yin ye.
-move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //; last first.
+move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //.
   by move=> [u1 u2] [v1 v2]; rewrite /f /=; case=> -> ->.
 move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h u.
 rewrite !mem_cat !in_cons orbA orbCA -!orbA; move: (h u); rewrite !mem_cat=> ->.
@@ -849,15 +849,15 @@ elim: neq1 lt1 oc2 => [|t1 neq1 ih] lt1 [eq2 neq2 lt2 leq2] /=.
 rewrite map_cat /= mem_cat -!map_comp; set f := fun _ => _.
 rewrite -/f in ih; case/orP.
   case/mapP=> y yin ye.
-  move: (ih lt1 (f y)); rewrite mem_map //; last first.
+  move: (ih lt1 (f y)); rewrite mem_map //.
     by move=> u v; rewrite /f /=; case.
   move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h.
   move=> u. rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA.
   case/orP; first by move->; rewrite !orbT.
   rewrite !orbA [_ || (_ \in eq1)]orbC; move: (h u); rewrite !mem_cat=> hu.
   by move/hu; do 2!(case/orP; last by move->; rewrite !orbT); move->.
 case/mapP=> y yin ye.
-move: (ih lt1 (f y)); rewrite mem_map //; last first.
+move: (ih lt1 (f y)); rewrite mem_map //.
   by move=> u v; rewrite /f /=; case.
 move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h.
 move=> u; rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA.

theories/polyorder.v

@@ -2,7 +2,7 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype ssralg zmodp poly polydiv ssrnum interval.
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 Import GRing.Theory Num.Theory Pdiv.Idomain.
 
@@ -85,7 +85,7 @@ Lemma root_muN p x : p != 0 ->
   (('X - x%:P)^+(\mu_x p).+1 %| p) = false.
 Proof.
 move=> pn0; case: (mu_spec x pn0)=> q qn0 hp /=.
-rewrite {2}hp exprS dvdp_mul2r; last first.
+rewrite {2}hp exprS dvdp_mul2r.
   by rewrite expf_neq0 // polyXsubC_eq0.
 apply: negbTE; rewrite -eqp_div_XsubC; apply: contra qn0.
 by move/eqP->; rewrite rootM root_XsubC eqxx orbT.
@@ -124,7 +124,7 @@ Qed.
 Lemma cofactor_XsubC_mu  x p n :
   ~~ root p x -> \mu_x (p * ('X - x%:P) ^+ n) = n.
 Proof.
-move=> p0; apply/eqP; rewrite eq_sym -muP//; last first.
+move=> p0; apply/eqP; rewrite eq_sym -muP//.
   apply: contra p0; rewrite mulf_eq0 expf_eq0 polyXsubC_eq0 andbF orbF.
   by move/eqP->; rewrite root0.
 rewrite dvdp_mulIr /= exprS dvdp_mul2r -?root_factor_theorem //.
@@ -147,7 +147,7 @@ Qed.
 
 Lemma mu_XsubC x : \mu_x ('X - x%:P) = 1%N.
 Proof.
-apply/eqP; rewrite eq_sym -muP; last by rewrite polyXsubC_eq0.
+apply/eqP; rewrite eq_sym -muP; first by rewrite polyXsubC_eq0.
 by rewrite expr1 dvdpp/= -{2}[_ - _]expr1 dvdp_Pexp2l // size_XsubC.
 Qed.
 
@@ -181,11 +181,11 @@ have qn0: q != 0 by move: mupq; apply: contraL; move/eqP->; rewrite mu0 ltn0.
 case: (mu_spec x pn0)=> [qqp qqp0] hp.
 case: (mu_spec x qn0)=> [qqq qqq0] hq.
 rewrite hp hq -(subnK (ltnW mupq)).
-rewrite mu_mul ?mulf_eq0; last first.
+rewrite mu_mul ?mulf_eq0.
   rewrite expf_eq0 polyXsubC_eq0 andbF orbF.
   by apply: contra qqp0; move/eqP->; rewrite root0.
 rewrite mu_exp mu_XsubC mul1n [\mu_x qqp]muNroot // add0n.
-rewrite exprD mulrA -mulrDl mu_mul; last first.
+rewrite exprD mulrA -mulrDl mu_mul.
   by rewrite mulrDl -mulrA -exprD subnK 1?ltnW // -hp -hq.
 rewrite muNroot ?add0n ?mu_exp ?mu_XsubC ?mul1n //.
 rewrite rootE !hornerE ?horner_exp ?hornerXsubC subrr.
@@ -204,8 +204,8 @@ move=> hn.
 case p0: (p == 0); first by rewrite (eqP p0) div0p mu0 sub0n.
 case: (@mu_spec p x); rewrite ?p0 // => q hq hp.
 rewrite {1}hp -{1}(subnK hn) exprD mulrA.
-rewrite Pdiv.IdomainMonic.mulpK; last by apply: monic_exp; apply: monicXsubC.
-rewrite mu_mul ?mulf_eq0 ?expf_eq0 ?polyXsubC_eq0 ?andbF ?orbF; last first.
+rewrite Pdiv.IdomainMonic.mulpK; first by apply: monic_exp; apply: monicXsubC.
+rewrite mu_mul ?mulf_eq0 ?expf_eq0 ?polyXsubC_eq0 ?andbF ?orbF.
   by apply: contra hq; move/eqP->; rewrite root0.
 by rewrite mu_exp muNroot // add0n mu_XsubC mul1n.
 Qed.
@@ -237,7 +237,7 @@ Lemma derivn_poly0 : forall (p : {poly R}) n, (size p <= n)%N = (p^`(n) == 0).
 Proof.
 move=> p n; apply/idP/idP.
    move=> Hpn; apply/eqP; apply/polyP=>i; rewrite coef_derivn.
-   rewrite nth_default; first by rewrite mul0rn coef0.
+   rewrite nth_default; last by rewrite mul0rn coef0.
    by apply: leq_trans Hpn _; apply leq_addr.
 elim: n {-2}n p (leqnn n) => [m | n ihn [| m]] p.
 - by rewrite leqn0; move/eqP->; rewrite derivn0 leqn0 -size_poly_eq0.
@@ -265,6 +265,3 @@ by move=> x p p0 rpx; rewrite mu_deriv // subn1 addn1 prednK // mu_gt0.
 Qed.
 
 End PolyrealIdomain.
-
-
-