Remove some unnecessary use of unitfE

[pi8027]

Motivation for this change

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

$ grep -n --color 'unitfE' $(git ls-files | grep '\.v$')
theories/charge.v:867:  by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE.
theories/charge.v:1590:  by rewrite unitfE gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure.
theories/derive.v:326:  by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0.
theories/derive.v:341:rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVr ?unitfE ?gt_eqF //.
theories/derive.v:342:rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first.
theories/derive.v:709:rewrite normfV ger0_norm /k // invrM ?unitfE // mulrAC mulVf //.
theories/derive.v:785:  rewrite invrM ?unitfE // [kv ^-1]invrM ?unitfE //.
theories/exp.v:992:  by rewrite /powR gt_eqF// -expRM_natl mulrA divrr ?mul1r ?unitfE// lnK.
theories/hoelder.v:209:    by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
theories/hoelder.v:211:  by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
theories/landau.v:1338:  rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
theories/landau.v:1500:  rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
theories/lebesgue_measure.v:628:      rewrite inE ltr0n andbT unitfE.
theories/lebesgue_measure.v:634:    by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
theories/measurable_realfun.v:1004:by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE.
theories/measure.v:3642:by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0.
theories/normedtype.v:1109:Proof. by rewrite -normr_eq0 -unitfE => /normrZV->. Qed.
theories/normedtype.v:2139:by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE.
theories/normedtype.v:4350:near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVr ?unitfE //.
theories/normedtype.v:4351:rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r.
theories/normedtype.v:4361:rewrite mul1r mulVr ?unitfE ?gt_eqF// ?ltr0n ?expn_gt0//.
theories/normedtype.v:4362:rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r.
theories/normedtype.v:5213:(*     rewrite mulrDl mul1r -mulrA mulVr ?unitfE ?lt0r_neq0 // mulr1. *)
theories/normedtype.v:5215:(*     by rewrite -mulrA mulrV ?mulr1 ?unitfE // subrK. *)
theories/normedtype.v:5236:(*     rewrite mulrDl mul1r -mulrA mulVr ?unitfE ?lt0r_neq0 // mulr1. *)
theories/normedtype.v:5238:(*     by rewrite -mulrA mulrV ?mulr1 ?unitfE // subrK. *)
theories/normedtype.v:5497:  rewrite -[X in X - _](@divrr _ `|x - y|) ?unitfE ?normr_eq0 ?subr_eq0//.
theories/normedtype.v:6323:  by rewrite invrM ?unitfE// mulrAC -mulrA (mulrA 2) divff// div1r.
theories/numfun.v:550:    by rewrite -lerBlDr -opprD -2!mulrDl natr1 divrr ?unitfE// mul1r.
theories/numfun.v:559:  by rewrite lerBlDl -2!mulrDl nat1r divrr ?mul1r// unitfE.
theories/numfun.v:581:Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divrr// unitfE. Qed.
theories/numfun.v:656:  by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE.
theories/probability.v:706:  by rewrite /u0 -mulrA mulVr ?mulr1 ?unitfE ?gt_eqF.
theories/sequences.v:854:    rewrite mulrC -normrV ?unitfE //.
theories/sequences.v:865:rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA.
theories/sequences.v:892:rewrite -[X in X - _](@divrr _ (n.+2)%:R) ?unitfE ?pnatr_eq0 //.
theories/sequences.v:996:  by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE.

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