Cleanup

Author: pi8027

classical/unstable.v

@@ -60,7 +60,7 @@ Proof.
 apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
 case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
   by rewrite addrCA addrK.
-by rewrite addrCA addrAC subrr add0r.
+by rewrite addrC subrKA.
 Qed.
 
 Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.

experimental_reals/distr.v

@@ -335,7 +335,7 @@ Definition mflip (xt : R) :=
 Lemma isd_mflip xt : isdistr (mflip xt).
 Proof. apply/isdistr_finP; split=> [b|].
 + by case: b; rewrite ?subr_ge0 cp01_clamp.
-+ by rewrite /index_enum !unlock /= addr0 addrCA subrr addr0.
++ by rewrite /index_enum !unlock /= addr0 addrC subrK.
 Qed.
 
 Definition dflip (xt : R) := locked (mkdistr (isd_mflip xt)).
@@ -1133,7 +1133,7 @@ Qed.
 
 Lemma pr_and A B mu : \P_[mu] [predI A & B] =
   \P_[mu] A + \P_[mu] B - \P_[mu] [predU A & B].
-Proof. by rewrite pr_or opprB addrCA subrr addr0. Qed.
+Proof. by rewrite pr_or subKr. Qed.
 
 Lemma ler_pr_or A B mu :
   \P_[mu] [predU A & B] <= \P_[mu] A + \P_[mu] B.

experimental_reals/realseq.v

@@ -122,7 +122,7 @@ have gt0_e: 0 < e by rewrite subr_gt0.
 move=> x y; rewrite !inE/= /eclamp pmulr_rle0 // invr_le0.
 rewrite lern0 /= !ltr_distl => /andP[_ lt1] /andP[lt2 _].
 apply/(lt_trans lt1)/(le_lt_trans _ lt2).
-by rewrite lerBrDl addrCA -splitr /e addrCA subrr addr0.
+by rewrite lerBrDl addrCA -splitr /e addrC subrK.
 Qed.
 
 Lemma separable {R : realType} (l1 l2 : \bar R) :
@@ -303,9 +303,8 @@ Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E ->
 Proof.
 move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S.
 have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)).
-  move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
-  rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr.
-  by rewrite !(mulrN, mulNr) (addrCA (lu * lv)) subrr addr0 subrr.
+  move=> n; rewrite {}/a {}/b /=.
+  by rewrite addrC mulrBr addrAC subrK addrC mulrBl subrK.
 apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD.
   by apply/ncvgC. rewrite -[X in X%:E]addr0; apply/ncvgD.
 + apply/ncvgMr; first rewrite -[X in X%:E](subrr lv).
@@ -388,7 +387,7 @@ case: l1 l2 => [l1||] [l2||] //=; first last.
 move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
 case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
 rewrite ltr_distl => /andP[] /(le_lt_trans _) h _; apply: h.
-by rewrite {cv}/e opprB addrCA subrr addr0.
+by rewrite {cv}/e subKr.
 Qed.
 
 Lemma ncvg_lt (u : nat -> R) (l1 l2 : \bar R) :

experimental_reals/realsum.v

@@ -465,8 +465,7 @@ apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first.
 move=> lt_xS; pose e := psum S - x.
   have ge0_e: 0 < e by rewrite subr_gt0.
 case: (sup_adherent ge0_e (summable_sup smS)) => y.
-case=> /= J ->; rewrite /e /psum (asboolT smS).
-rewrite opprB addrCA subrr addr0 => lt_xSJ.
+case=> /= J ->; rewrite /e /psum (asboolT smS) subKr => lt_xSJ.
 pose k := \max_(j : J) (val j); have lt_x_uSk: x < u k.+1.
   apply/(lt_le_trans lt_xSJ); rewrite /u big_ord_mkfset.
   rewrite (eq_bigr (S \o val)) => /= [j _|]; first by rewrite ger0_norm.

reals/reals.v

@@ -281,8 +281,7 @@ Qed.
 Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.
 Proof.
 move=> hasE leEx; set y := sup E; pose z := (x + y) / 2%:R.
-have Dz: 2%:R * z = x + y.
-  by rewrite mulrCA divff ?mulr1 // pnatr_eq0.
+have Dz: 2%:R * z = x + y by rewrite mulrC divfK// pnatr_eq0.
 have ubE : has_sup E by split => //; exists x.
 have [/downP [t Et lezt] | leyz] := sup_total z ubE.
   rewrite -(lerD2l x) -Dz -mulr2n -[leRHS]mulr_natl.
@@ -334,8 +333,7 @@ have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
 have [r Ar supBr] := sup_adherent e2pos supA.
 have [s Bs supAs] := sup_adherent e2pos supB.
 have := ltrD supBr supAs.
-rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA.
-rewrite subrr add0r; apply/negP; rewrite -leNgt.
+rewrite -addrACA -opprD -splitr subKr; apply/negP; rewrite -leNgt.
 by apply: sup_upper_bound => //; exists r => //; exists s.
 Qed.