Cleanup some proofs (math-comp#1407)

classical/mathcomp_extra.v

@@ -156,14 +156,14 @@ Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.
 Proof.
 apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
 case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
-  by rewrite addrACA subrr addr0.
+  by rewrite addrCA addrK.
 by rewrite addrCA addrAC subrr add0r.
 Qed.
 
 Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.
 Proof.
 apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *)
-by rewrite -mulrDl addrACA subrr addr0 mulrDl -splitr.
+by rewrite -mulrDl addrCA addrK mulrDl -splitr.
 Qed.
 
 End max_min.
@@ -304,8 +304,7 @@ Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed.
 
 Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed.
 
-Lemma onemK r : `1-(`1-r) = r.
-Proof. by rewrite /onem opprB addrCA subrr addr0. Qed.
+Lemma onemK r : `1-(`1-r) = r. Proof. exact: subKr. Qed.
 
 Lemma add_onemK r : r + `1- r = 1.
 Proof. by rewrite /onem addrC subrK. Qed.

classical/set_interval.v

@@ -540,7 +540,7 @@ Lemma line_path1 a b : line_path a b 1 = b.
 Proof. by rewrite /line_path subrr mul0r add0r mul1r. Qed.
 
 Lemma line_path_sym a b t : line_path a b t = line_path b a (1 - t).
-Proof. by rewrite /line_path opprB addrCA subrr addr0 addrC. Qed.
+Proof. by rewrite /line_path subKr addrC. Qed.
 
 Lemma line_path_flat a : line_path a a = cst a.
 Proof. by apply/funext => t; rewrite line_pathEl subrr mulr0 add0r. Qed.

reals/itv.v

@@ -888,10 +888,7 @@ Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
   (1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01.
 
 Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
-Proof.
-apply/val_inj => /=.
-by rewrite subr0 mulr1 opprB addrCA subrr addr0.
-Qed.
+Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed.
 
 Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
   @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].

reals/reals.v

@@ -81,8 +81,7 @@ Proof. by rewrite predeqE => r; split => // _. Qed.
 Lemma lboundT : lbound [set: R] = set0.
 Proof.
 rewrite predeqE => r; split => // /(_ (r - 1) Logic.I).
-rewrite lerBrDl addrC -lerBrDl subrr.
-by rewrite real_leNgt ?realE ?ler01// ?lexx// ltr01.
+by rewrite addrC -subr_ge0 addrK ler0N1.
 Qed.
 
 End subr_image.
@@ -277,8 +276,7 @@ Proof.
 move=> has_supE; rewrite orC.
 case: (lerP (sup E) x)=> hx /=; [by left|right].
 have /sup_adherent/(_  has_supE) : 0 < sup E - x by rewrite subr_gt0.
-case=> e Ee hlte; apply/downP; exists e => //; move: hlte.
-by rewrite opprB addrCA subrr addr0 => /ltW.
+by case=> e Ee; rewrite subKr => /ltW hlte; apply/downP; exists e.
 Qed.
 
 Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.
@@ -452,7 +450,7 @@ rewrite le_eqVlt=> /orP[/eqP<-//| lt_yFx].
 rewrite ltrBlDr -ltrBlDl => lt1_FxBy.
 pose e := sup (floor_set x) - y; have := has_sup_floor_set x.
 move/sup_adherent=> -/(_ e) []; first by rewrite subr_gt0.
-move=> z Fz; rewrite /e opprB addrCA subrr addr0 => lt_yz.
+move=> z Fz; rewrite /= subKr => lt_yz.
 have /sup_upper_bound /ubP /(_ _ Fz) := has_sup_floor_set x.
 rewrite -(lerD2r (-y)) => /le_lt_trans /(_ lt1_FxBy).
 case/andP: Fy Fz lt_yz=> /RintP[yi -> _].
@@ -644,7 +642,7 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l :
   exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x.
 Proof.
 set P := [set y | _]; move=> hs; rewrite -subr_gt0.
-move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
+move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrC subrK => ltFxl.
 by exists x => //; rewrite (inf_lbound hs.2)//; exists x.
 Qed.
 

theories/derive.v

@@ -254,7 +254,7 @@ Proof.
 move=> df; apply/eqaddoP => _/posnumP[e].
 rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
   rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r.
-  by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0.
+  by rewrite addrCA addKr normrN scale0r !normr0 mulr0.
 have /eqolimP := df.
 move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
 apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
@@ -973,7 +973,7 @@ rewrite normrN [leRHS]ger0_norm; last first.
   rewrite subr_ge0; apply: ltW; apply: lt_le_trans lthhx _.
   by rewrite ler_pdivrMr // -{1}(mulr1 `|x|) ler_pM // ler1n.
 rewrite lerBrDr -lerBrDl (splitr `|x|).
-by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltW.
+by rewrite normrM normfV (@ger0_norm _ 2) // addrK; apply/ltW.
 Unshelve. all: by end_near. Qed.
 
 Lemma diff_Rinv (x : R) : x != 0 ->
@@ -1569,15 +1569,14 @@ Proof.
 move=> altb fdrvbl fcont.
 set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl x : x \in `]a, b[%R -> derivable g x 1.
-  by move=> /fdrvbl dfx; apply: derivableB => //; exact/derivable1_diffP.
+  by move=> /fdrvbl dfx; apply/derivableB/derivable1_diffP.
 have gcont : {within `[a, b], continuous g}.
-  move=> x; apply: continuousD _ ; first by move=>?; exact: fcont.
-  by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous.
+  move=> x; apply: continuousD _ ; first exact: fcont.
+  exact/continuousN/continuous_subspaceT/scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
-  rewrite [_ *: _]mulrA mulrC mulrA mulVf.
-    by rewrite mul1r addrCA subrr addr0.
+  rewrite [_ *: _]mulrC divfK; first by rewrite addrC subrK.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
 exists c; first exact: cab.

theories/lebesgue_integral.v

@@ -348,8 +348,8 @@ Lemma sfun_rect (K : T -> Type) :
   (forall f (Pf : f \in sfun), K (sfun_Sub Pf)) -> forall u : T, K u.
 Proof.
 move=> Ksub [f [[Pf1] [Pf2]]]; have Pf : f \in sfun by apply/andP; rewrite ?inE.
-have -> : Pf1 = (set_mem (sub_sfun_mfun Pf)) by [].
-have -> : Pf2 = (set_mem (sub_sfun_fimfun Pf)) by [].
+have -> : Pf1 = set_mem (sub_sfun_mfun Pf) by [].
+have -> : Pf2 = set_mem (sub_sfun_fimfun Pf) by [].
 exact: Ksub.
 Qed.
 
@@ -451,24 +451,18 @@ Qed.
 Lemma preimage_cstM T (R : realFieldType) (x y : R) (f : T -> R) :
   x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].
 Proof.
-move=> x0; apply/seteqP; rewrite /preimage; split => [z/= <-|z/= ->].
-  by rewrite mulrAC divrr ?mul1r// unitfE.
-by rewrite mulrCA divrr ?mulr1// unitfE.
+move=> x0; apply/seteqP.
+by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK).
 Qed.
 
 Lemma preimage_add T (R : numDomainType) (f g : T -> R) z :
   (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT)
     ((f @^-1` [set a]) `&` (g @^-1` [set z - a])).
 Proof.
-apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] []].
-  have : z - f x \in g @` setT.
-    by rewrite inE /=; exists x=> //; rewrite -fgz addrC addKr.
-  rewrite inE /= => -[x' _ gzf]; exists (z - g x')%R => /=.
-    by exists x => //; rewrite gzf opprB addrC subrK.
-  rewrite /preimage /=; split; first by rewrite gzf opprB addrC subrK.
-  by rewrite gzf opprB addrC subrK -fgz addrC addKr.
-rewrite /preimage /= => [fxfy gzf].
-by rewrite gzf -fxfy addrC subrK.
+apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] [fxfy gzf]]; last first.
+  by rewrite gzf -fxfy addrC subrK.
+exists (z - g x); first by exists x; rewrite // -fgz addrK.
+by split; rewrite 1?subKr // -fgz addrK.
 Qed.
 
 Section simple_bounded.
@@ -483,6 +477,7 @@ exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
 split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
 have ? : f z \in r by have := imageT f z; rewrite fr.
 rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
+  (* TODO: generalize the statement of bigmaxe_fin_num *)
   have := @bigmaxe_fin_num _ (map normr r) `|f z|.
   by rewrite big_map => ->//; apply/mapP; exists (f z).
 by rewrite (bigmax_sup_seq _ _ (lexx _)).
@@ -586,14 +581,14 @@ Import HBNNSimple.
 Lemma nnsfun_cover : \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT.
 Proof. by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed.
 
-Lemma nnsfun_coverT :
-  \big[setU/set0]_(i \in [set: R]) (f @^-1` [set i]) = setT.
+Lemma nnsfun_coverT : \big[setU/set0]_(i \in [set: R]) f @^-1` [set i] = setT.
 Proof.
-by rewrite -(fsbig_widen (range f)) ?nnsfun_cover//= => x [_ /= /preimage10->].
+by rewrite -(fsbig_widen (range f)) ?nnsfun_cover//= => x [_ /preimage10].
 Qed.
 
 End nnsfun_cover.
 
+(* FIXME: shouldn't we avoid calling [done] in a hint? *)
 #[global] Hint Extern 0 (measurable (_ @^-1` [set _])) =>
   solve [apply: measurable_sfunP; exact: measurable_set1] : core.
 
@@ -626,8 +621,8 @@ Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x :
   m (f @^-1` [set x] `&` \big[setU/set0]_(i \in range g) (g @^-1` [set i])).
 Proof.
 rewrite -?measure_fsbig//.
-- by rewrite !fsbig_finite//= big_distrr//.
-- by move=> i Ai; apply: measurableI => //.
+- by rewrite !fsbig_finite//= big_distrr.
+- by move=> i Ai; apply: measurableI.
 - exact/trivIset_setIl/trivIset_preimage1.
 Qed.
 
@@ -644,8 +639,8 @@ Local Open Scope ereal_scope.
 Let mulef_ge0 (R : realDomainType) x (f : R -> \bar R) :
   0 <= f x -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x.
 Proof.
-move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (xA x0) mule0.
-by rewrite mule_ge0.
+case: (ltP x 0%R) => [x_lt0 ? ->|x_ge0 fx_ge0 _] //; last exact: mule_ge0.
+by rewrite mule0.
 Qed.
 
 Lemma nnfun_muleindic_ge0 d (T : sigmaRingType d) (R : realDomainType)
@@ -717,11 +712,11 @@ Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed.
 
 Lemma sintegral_indic (A : set T) : sintegral mu \1_A = mu A.
 Proof.
-rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //; last 2 first.
+rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //=; last 2 first.
   - exact: image_indic_sub.
   - by move=> t [[] -> /= /preimage10->]; rewrite measure0 mule0.
-have N01 : (0 <> 1:> R)%R by move=> /esym/eqP; rewrite oner_eq0.
-rewrite fsbigU//=; last by move=> t [->]//.
+have N01 : (0 <> 1:> R)%R by apply/eqP; rewrite eq_sym oner_eq0.
+rewrite fsbigU//=; last by move=> t [->].
 rewrite !fsbig_set1 mul0e add0e mul1e.
 by rewrite preimage_indic ifT ?inE// ifN ?notin_setE.
 Qed.
@@ -732,8 +727,8 @@ Lemma sintegralEnnsfun (f : {nnsfun T >-> R}) : sintegral mu f =
 Proof.
 rewrite (fsbig_widen _ setT) ?sintegralET//.
 move=> x [_ /=]; case: ltgtP => //= [xlt0 _|<-]; last by rewrite mul0e.
-rewrite preimage10 ?measure0 ?mule0//= => -[t _].
-by apply/eqP; apply: contra_ltN xlt0 => /eqP<-.
+rewrite preimage10 ?measure0 ?mule0//= => -[t _ xE].
+by apply/negP: xlt0; rewrite -leNgt -xE.
 Qed.
 
 End sintegral_lemmas.
@@ -755,14 +750,10 @@ Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f.
 Proof.
 have [->|r0] := eqVneq r 0%R.
   by rewrite mul0e (eq_sintegral (cst 0%R)) ?sintegral0// => x/=; rewrite mul0r.
-rewrite !sintegralET.
-transitivity (\sum_(x \in [set: R]) x%:E * m (f @^-1` [set x / r])).
-  by under eq_fsbigr do rewrite preimage_cstM//.
-transitivity (\sum_(x \in [set: R]) r%:E * (x%:E * m (f @^-1` [set x]))).
-  rewrite (reindex_fsbigT (fun x => r * x)%R)//; last first.
-    by exists ( *%R r ^-1)%R; [exact: mulKf|exact: mulVKf].
-  by apply: eq_fsbigr => x; rewrite mulrAC divrr ?unitfE// mul1r muleA EFinM.
-by rewrite ge0_mule_fsumr// => x; exact: nnsfun_mulemu_ge0.
+rewrite !sintegralET ge0_mule_fsumr; last exact: nnsfun_mulemu_ge0.
+rewrite (reindex_fsbigT ( *%R r))/=; last first.
+  by exists ( *%R r^-1); [exact: mulKf|exact: mulVKf].
+by apply: eq_fsbigr => x; rewrite preimage_cstM// [_ / r]mulrC mulKf// muleA.
 Qed.
 
 End sintegralrM.
@@ -783,7 +774,7 @@ transitivity (\sum_(z \in FG) z%:E * \sum_(a \in F) m (pf a `&` pg (z - a)%R)).
   apply: eq_fsbigr => z _; rewrite preimage_add -fsbig_setU// measure_fsbig//.
     by move=> x Fx; exact: measurableI.
   exact/trivIset_setIr/trivIset_preimage1.
-under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//.
+under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//=.
 transitivity (\sum_(x \in F) \sum_(y \in G) (x + y)%:E * m (pf x `&` pg y)).
   apply: eq_fsbigr => x _; rewrite /pf /pg (fsbig_widen G setT)//=; last first.
     by move=> y [_ /= /preimage10->]; rewrite setI0 measure0 mule0.

theories/separation_axioms.v

@@ -845,12 +845,10 @@ move: x e1 e2; elim: n.
   move=> x e1 e2 e1e2 y [?] gxy; split; first exact: (lt_le_trans _ e1e2).
   by apply: descendG; last (exact: gxy); exact: distN_le.
 move=> n IH x e1 e2 e1e2 z [y] [d1] [d2] [] /IH P d1pos d2pos gyz d1d2e1.
-have d1e1d2 : d1 = e1 - d2 by rewrite -d1d2e1 -addrA subrr addr0.
-have e2d2le : e1 - d2 <= e2 - d2 by exact: lerB.
 exists y, (e2 - d2), d2; split => //.
-- by apply: P; apply: le_trans e2d2le; rewrite d1e1d2.
-- by apply: lt_le_trans e2d2le; rewrite -d1e1d2.
-- by rewrite -addrA [-_ + _]addrC subrr addr0.
+- by apply: P; rewrite lerBrDr d1d2e1.
+- by apply: lt_le_trans d1pos _; rewrite lerBrDr d1d2e1.
+- by rewrite subrK.
 Qed.
 
 Local Lemma step_ball_le x e1 e2 :
@@ -901,15 +899,13 @@ case: (pselect (e2 <= d2)).
     by rewrite -deE lerDr; exact: ltW.
   - exact: n_step_ball_center.
   - by rewrite addn0.
-have d1E' : d1 = e1 + (e2 - d2).
-  by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0.
+have d1E' : d1 = e1 + (e2 - d2) by rewrite addrA -deE addrK.
 move=> /negP; rewrite -ltNge// => d2lee2.
   case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
   move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
   exists t1, t2, c1, c2.+1; split => //.
   - by apply: (@n_step_ball_le _ _ d1); rewrite -?deE // ?lerDl; exact: ltW.
-  - exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0//.
-    by rewrite -addrA [-_ + _]addrC subrr addr0.
+  - by exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0// subrK.
   - by rewrite addnS.
 Qed.
 

theories/sequences.v

@@ -563,7 +563,7 @@ Proof. by rewrite seriesEnat/= -big_cat_nat// leq_addl. Qed.
 
 Lemma sub_series_geq m n : (m <= n)%N ->
   series n - series m = \sum_(m <= k < n) u_ k.
-Proof. by move=> /subnK<-; rewrite series_addn addrAC subrr add0r. Qed.
+Proof. by move=> /subnK<-; rewrite series_addn addrC addKr. Qed.
 
 Lemma sub_series m n :
   series n - series m = if (m <= n)%N then \sum_(m <= k < n) u_ k
@@ -3112,7 +3112,7 @@ have majball : forall f x, F f -> (ball x0 r%:num) x -> `|f (x - x0)| <= n%:R +
   apply/(le_trans (ler_normB _ _))/lerD; first exact: majballi.
   by apply: majballi => //; exact/ball_center.
 have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y  + x0).
-  rewrite -ball_normE /ball_ /= opprD addrCA subrr addr0 normrN normrZ.
+  rewrite -ball_normE /ball_ /= opprD addrC subrK normrN normrZ.
   rewrite 2!normrM -2!mulrA (@normfV _ `|y|) normr_id mulVf ?mulr1 ?normr_eq0//.
   by rewrite gtr0_norm // gtr0_norm // gtr_pMl // invf_lt1 // ltr1n.
 have := majball f (2^-1 * (r%:num / `|y|) *: y + x0) Ff ballprop.

theories/topology_theory/num_topology.v

@@ -44,21 +44,18 @@ case => [][[[]l|[]]] [[]r|[]] [[]]//= _.
   apply/(subset_trans _ lrU)/subset_ball_prop_in_itv.
   suff : (`]x - Order.min (x - l) (r - x), x + Order.min (x - l) (r - x)[
           <= `]l, r[)%O by move/subitvP => H ? ?; exact: H.
-  apply/andP; rewrite lteBSide; split => /=.
-    apply: (@le_trans _ _ (x - (x - l))); last by rewrite lerB // ge_min lexx.
-    by rewrite opprB addrCA subrr addr0.
-  apply: (@le_trans _ _ (x + (r - x))); last by rewrite addrCA subrr addr0.
-  by rewrite lerD // ge_min lexx orbT.
+  rewrite subitvE 2!lteBSide/=.
+  by rewrite lerBrDl [_ + l]addrC -2!lerBrDl 2!ge_min 2!lexx orbT.
 - move=> xl lU; exists (x - l) => /=; first by rewrite lterBDr add0r (itvP xl).
   apply/(subset_trans _ lU)/subset_ball_prop_in_itv.
   suff : (`]x - (x - l), x + (x - l)[ <= `]l, +oo[)%O.
     by move/subitvP => H ?; exact: H.
-  by apply/andP; rewrite lteBSide/=; split; rewrite // opprB addrCA subrr addr0.
+  by rewrite subitvE lteBSide/= subKr lexx.
 - move=> xr rU; exists (r - x) => /=; first by rewrite lterBDr add0r (itvP xr).
   apply/(subset_trans _ rU)/subset_ball_prop_in_itv.
   suff : (`]x - (r - x), x + (r - x)[ <= `]-oo, r[)%O.
     by move/subitvP => H ?; exact: H.
-  by apply/andP; rewrite lteBSide/=; split; rewrite // addrCA subrr addr0.
+  by rewrite subitvE lteBSide/= addrC subrK.
 - by move=> _; rewrite set_itvE subTset => ->; exists 1 => /=.
 Qed.
 

theories/trigo.v

@@ -838,7 +838,7 @@ Lemma cos2_tan2 x : cos x != 0 -> (cos x) ^- 2 = 1 + (tan x) ^+ 2.
 Proof.
 move=> cosx.
 rewrite /tan exprMn [X in _ = 1 + X * _]sin2cos2 mulrBl -exprMn divff //.
-by rewrite expr1n addrCA subrr addr0 mul1r exprVn.
+by rewrite expr1n addrC subrK mul1r exprVn.
 Qed.
 
 Lemma tan_pihalf : tan (pi / 2) = 0.