Cleanup (#1763)

* Cleanup

Author: pi8027

CHANGELOG_UNRELEASED.md

@@ -7,6 +7,9 @@
 - in `cardinality.v`:
   + lemma `infinite_setD`
 
+- in `convex.v`:
+  + lemmas `convN`, `conv_le`
+
 ### Changed
 
 ### Renamed

analysis_stdlib/Rstruct_topology.v

@@ -7,11 +7,9 @@
 Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
 Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
 Require Import Rtrigo1 Reals.
-From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
-From mathcomp Require Import archimedean.
 From HB Require Import structures.
-From mathcomp Require Import mathcomp_extra boolp classical_sets.
-From mathcomp Require Import reals interval_inference.
+From mathcomp Require Import all_ssreflect ssralg ssrnum archimedean.
+From mathcomp Require Import boolp classical_sets reals interval_inference.
 From mathcomp Require Export Rstruct.
 From mathcomp Require Import topology.
 (* The following line is for RexpE. *)

classical/filter.v

@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
-From mathcomp Require Import archimedean.
+From mathcomp Require Import all_ssreflect all_algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 

classical/mathcomp_extra.v

@@ -1,6 +1,5 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
-From mathcomp Require Import archimedean rat finset interval.
+From mathcomp Require Import all_ssreflect finmap ssralg ssrnum.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)

classical/set_interval.v

@@ -569,13 +569,10 @@ Lemma line_path_id : line_path 0 1 = id.
 Proof. by apply/funext => t; rewrite /line_path mulr0 add0r mulr1. Qed.
 
 Lemma line_pathEl a b t : line_path a b t = t * (b - a) + a.
-Proof. by rewrite /line_path mulrBl mul1r mulrBr addrAC [RHS]addrC addrA. Qed.
+Proof. by rewrite /line_path mulrBl addrAC -addrA -mulrBr mul1r addrC. Qed.
 
 Lemma line_pathEr a b t : line_path a b t = (1 - t) * (a - b) + b.
-Proof.
-rewrite /line_path mulrBr -addrA; congr (_ + _).
-by rewrite mulrBl opprB mul1r addrNK.
-Qed.
+Proof. by rewrite mulrBl mul1r addrAC subrK -mulrN opprB addrC line_pathEl. Qed.
 
 Lemma line_path10 t : line_path 1 0 t = 1 - t.
 Proof. by rewrite /line_path mulr0 addr0 mulr1. Qed.

classical/unstable.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp Require Import archimedean finset interval mathcomp_extra.
+From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
+From mathcomp Require Import archimedean interval mathcomp_extra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -277,16 +277,13 @@ 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.
 
 Lemma onemD r s : `1-(r + s) = `1-r - s.
-Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed.
+Proof. by rewrite /onem opprD addrA. Qed.
 
 Lemma onemMr r s : s * `1-r = s - s * r.
 Proof. by rewrite /onem mulrBr mulr1. Qed.
 
 Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s.
-Proof.
-rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA.
-by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK.
-Qed.
+Proof. by rewrite /onem mulrBl 2!mulrBr !mul1r mulr1 addrKA opprK subrKA. Qed.
 
 End onem_ring.
 

experimental_reals/distr.v

@@ -286,7 +286,7 @@ Local Lemma mrat_sup s : (0 < size s)%N ->
 Proof.
 move=> gt0_s; rewrite -mulr_suml -natr_sum.
 apply/(mulIf (x := (size s)%:R)); first by rewrite pnatr_eq0 -lt0n.
-rewrite mul1r -mulrA mulVf ?mulr1 ?pnatr_eq0 -?lt0n //; congr (_%:R).
+rewrite mul1r divfK ?pnatr_eq0 -?lt0n//; congr (_%:R).
 rewrite -sum1_size -[in RHS]big_undup_iterop_count/=; apply: eq_bigr => i _.
 by rewrite Monoid.iteropE iter_addn addn0 mul1n.
 Qed.

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 addrC subrK.
+by rewrite lerBrDr -addrA -splitr subrKC.
 Qed.
 
 Lemma separable {R : realType} (l1 l2 : \bar R) :
@@ -303,8 +303,7 @@ 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 /=.
-  by rewrite addrC mulrBr addrAC subrK addrC mulrBl subrK.
+  by move=> n; rewrite /= addrA mulrBr mulrBl 2!subrKC.
 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).

experimental_reals/realsum.v

@@ -3,7 +3,7 @@
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect all_algebra archimedean.
+From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
@@ -14,7 +14,6 @@ Unset Printing Implicit Defensive.
 Unset SsrOldRewriteGoalsOrder.
 
 Import Order.TTheory GRing.Theory Num.Theory.
-From mathcomp.classical Require Import mathcomp_extra.
 
 Local Open Scope fset_scope.
 Local Open Scope ring_scope.

reals/real_interval.v

@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import fingroup perm rat archimedean finmap.
+From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval.
+From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Export set_interval.
-From HB Require Import structures.
 From mathcomp Require Import reals interval_inference constructive_ereal.
 
 (**md**************************************************************************)
@@ -14,7 +13,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-From mathcomp Require Import mathcomp_extra unstable.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.