Cleanup

[pi8027]

Motivation for this change

The same simplification should apply to (most of) the following lines:

$ grep -n --color '\(subrr add\(0r\|r0\)\|div\(rr\|ff\) ?mul\(1r\|r1\)\)' $(git ls-files | grep '\.v$')
theories/convex.v:217:  by exists z => //; rewrite fbfx -mulrA divff ?mulr1// subr_eq0 gt_eqF.
theories/convex.v:229:  by rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF.
theories/convex.v:269:  by rewrite mulrCA divff ?mulr1// subr_eq0 gt_eqF.
theories/derive.v:1894:- rewrite -ball_normE/= opprD addrCA subrr addr0 normrN normrZ ltr_pM2l//.
theories/ereal.v:1044:rewrite -ltrBlDl addrAC subrr add0r ltrNl opprK -lte_fin.
theories/ereal.v:1183:    move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0.
theories/ereal.v:1201:        by rewrite reN1 addrAC subrr add0r.
theories/ereal.v:1234:    rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl.
theories/ereal.v:1290:          by apply; rewrite opprB addrCA subrr addr0.
theories/ereal.v:1311:        rewrite opprB ltrBrDl addrCA subrr addr0 => h.
theories/ereal.v:1317:      rewrite opprB ltrBrDl addrCA subrr addr0 => h.
theories/ereal.v:1364:      rewrite subrr add0r -/(contract M%:E).
theories/exp.v:950:by rewrite -{1}(powRr1 (ltW x0))// -powRD addrCA subrr addr0// gt_eqF.
theories/exp.v:992:  by rewrite /powR gt_eqF// -expRM_natl mulrA divrr ?mul1r ?unitfE// lnK.
theories/exp.v:1026:rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1).
theories/exp.v:1027:rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF//.
theories/ftc.v:81:    by rewrite -EFinD addrAC subrr add0r.
theories/ftc.v:135:    by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r.
theories/ftc.v:425:rewrite -addrAC subrr add0r (le_trans (le_normr_Rintegral _ _))//.
theories/ftc.v:466:    by rewrite opprB addrCA subrr addr0.
theories/hoelder.v:308:  rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0.
theories/hoelder.v:464:      rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//.
theories/hoelder.v:469:    + by rewrite invf_div -onemV ?gt_eqF// addrCA subrr addr0.
theories/hoelder.v:483:    + by rewrite invrK addrCA subrr addr0.
theories/landau.v:424:  by rewrite addrAC subrr add0r; apply: fg_o_e.
theories/landau.v:628:  by rewrite addrAC subrr add0r; apply: fg_o_e.
theories/lebesgue_integral_theory/lebesgue_Rintegral.v:232:  rewrite subrr add0r Rintegral_itv_obnd_cbnd//.
theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v:209:  by rewrite opprD opprK addrACA subrr add0r.
theories/lebesgue_integral_theory/lebesgue_integral_under.v:175:      by apply/funext => n; rewrite /x fctE addrAC subrr add0r addnC.
theories/lebesgue_measure.v:638:near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//.
theories/lebesgue_measure.v:764:by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
theories/lebesgue_measure.v:772:rewrite subrr add0r gtrN// ?mulr_gt0// -EFinD; congr (_%:E).
theories/lebesgue_measure.v:773:by rewrite opprB addrAC addrCA subrr addr0 -mulr2n.
theories/normedtype.v:1292:by rewrite /= ltr_distlC addrCA subrr addr0 => /andP[].
theories/normedtype.v:5199:(*       by rewrite addrCA subrr addr0. *)
theories/normedtype.v:5222:(*       by rewrite addrCA subrr addr0. *)
theories/normedtype.v:5393:(* by apply: eq_near => e; rewrite ![_ + e]addrC addrACA subrr addr0. *)
theories/normedtype.v:5605:  rewrite distrC addrAC subrr add0r normrZ normr_id.
theories/numfun.v:559:  by rewrite lerBlDl -2!mulrDl nat1r divrr ?mul1r// unitfE.
theories/numfun.v:633:    rewrite telescope_sumr //= addrCA subrr addr0.
theories/numfun.v:656:  by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE.
theories/pi_irrational.v:87:rewrite /f coefZ mulrA divff ?mul1r ?pnatr_eq0 ?gtn_eqF ?fact_gt0//.
theories/pi_irrational.v:124:by rewrite -mul_polyC bap opprB addrCA subrr addr0 mul_polyC.
theories/probability.v:893:by rewrite !fsbig_set1/= -EFinD addrCA subrr addr0.
theories/realfun.v:2539:    by rewrite ltrBrDr -addrA [-_ + _]addrC subrr addr0 => /ltW.
theories/realfun.v:2928:by rewrite -mulrA divff ?mulr1//; exact: dg0.
theories/trigo.v:487:Proof. by rewrite /pi -[_ *+ 2]mulr_natr -mulrA divff ?mulr1. Qed.

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels