adapt to MC#1256

math-comp · Aug 5, 2024 · 657d491 · 657d491
1 parent 9472b06
commit 657d491
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 8 deletions.
diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v
@@ -123,7 +123,7 @@ have [->|p_neq0] := eqVneq p 0.
   rewrite size_poly0 big_ord0 horner0 subr0 normr0 mulr_ge0 ?normr_ge0 //.
   by rewrite big_ord0 mulr0 lexx.
 rewrite -[size _]prednK ?lt0n ?size_poly_eq0 //.
-rewrite big_ord_recl expr0 mulr1 nderivn0 addrC addKr !mulr_sumr.
+rewrite big_ord_recl expr0 mulr1 nderivn0 [X in `|X|]addrC addKr !mulr_sumr.
 have := le_trans (ler_norm_sum _ _ _); apply.
 rewrite ler_sum // => i _.
 rewrite exprSr mulrA !normrM mulrC ler_wpM2l ?normr_ge0 //.
@@ -362,11 +362,11 @@ have [] := lerP=> /= a1N; have [] := lerP=> //= a1P;
 have [] := lerP=> //= a2P; rewrite ?(andbF, andbT) //; symmetry.
   rewrite ltW // (le_lt_trans _ a1P) //.
   rewrite (monoLR (addrK _) (lerD2r _)) -addrA.
-  rewrite (monoRL (addNKr _) (lerD2l _)) addrC.
+  rewrite (monoRL (addNKr _) (lerD2l _)) [leLHS]addrC.
   by rewrite (le_trans _ le_ar) // ler_normr opprB lexx orbT.
 rewrite ltW // (lt_le_trans a1N) //.
 rewrite (monoLR (addrK _) (lerD2r _)) -addrA.
-rewrite (monoRL (addNKr _) (lerD2l _)) addrC ?[r2 + _]addrC.
+rewrite (monoRL (addNKr _) (lerD2l _)) [leRHS]addrC [leLHS]addrC.
 by rewrite (le_trans _ le_ar) // ler_normr lexx.
 Qed.
 

diff --git a/theories/complex.v b/theories/complex.v
@@ -334,16 +334,16 @@ rewrite [X in _ <= X] sqrrD ?sqr_sqrtr;
    do ?by rewrite ?(ler_wpDr, sqrtr_ge0, sqr_ge0, mulr_ge0) //.
 rewrite -addrA addrCA (monoRL (addrNK _) (lerD2r _)) !sqrrD.
 set u := _ *+ 2; set v := _ *+ 2.
-rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -addrA.
-rewrite [u + _] addrC [X in _ - X]addrAC [b ^+ _ + _]addrC.
+rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -[X in X - _]addrA.
+rewrite [u + _]addrC [X in _ - X]addrAC [b ^+ _ + _]addrC.
 rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _).
-rewrite -addrA addrC addKr -!lock addrC.
+rewrite -addrA addrC addrK -!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.
   by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //.
 rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_wpDr, sqr_ge0) //.
-rewrite -mulrnDl -mulr_natl !exprMn ler_pM2l ?exprn_gt0 ?ltr0n //.
+rewrite -mulrnDl -[in leLHS]mulr_natl !exprMn ler_pM2l ?exprn_gt0 ?ltr0n //.
 rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA lerD2l !addrA.
 rewrite [_ + (b * d) ^+ 2]addrC -addrA lerD2l.
 have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0.

diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v
@@ -287,7 +287,8 @@ rewrite !(expr0,expr1,mulr1) /=.
 case: j=> [] [|[|[|j]]] hj //.
 * by rewrite !mxE /= mulr0 add0r mulr1 mulrN1 addr0 taq_constraint1.
 * by rewrite !mxE /= mulr0 !mulr1 add0r addr0 taq_constraint2.
-* by rewrite !mxE /= addrA (@taq_constraint0 _ q) !mulr1 addr0 -addrA addrC.
+* rewrite !mxE /= addrA (@taq_constraint0 _ q) !mulr1 addr0 -[LHS]addrA.
+  exact/addrC.
 Qed.
 
 Lemma cvec_rec z q sq :