running semi-automated linting on the whole library

10 files changed, 26 insertions, 24 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 67454ac..941b488 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -403,7 +403,7 @@ Variable (T : Type) (zero one : T) (mul add : T -> T -> T) (inv : T -> T).
 Hypothesis mulC : commutative mul.
 
 Lemma mulC_id : left_id one mul -> right_id one mul.
-Proof. by move=>  mul1x x; rewrite mulC. Qed.
+Proof. by move=> mul1x x; rewrite mulC. Qed.
 
 Lemma mulC_zero : left_zero zero mul -> right_zero zero mul.
 Proof. by move=> mul0x x; rewrite mulC. Qed.
@@ -1596,7 +1596,7 @@ case: (pickP J) => [j0 _ | J0]; first exact: (big_distr_big_dep j0).
 rewrite {1 4}/index_enum -enumT; case: (enum I) (mem_enum I) => [I0 | i r _].
   have f0: I -> J by move=> i; have:= I0 i.
   rewrite (big_pred1 (finfun f0)) ?big_nil // => g.
-  by apply/familyP/eqP=> _; first apply/ffunP; move=> i; have:= I0 i.
+  by apply/familyP/eqP=> _; first apply/ffunP; move => i; have:= I0 i.
 have Q0 i': Q i' =1 pred0 by move=> j; have:= J0 j.
 rewrite big_cons /= big_pred0 // mul0m big_pred0 // => f.
 by apply/familyP=> /(_ i); rewrite [_ \in _]Q0.
@@ -1762,7 +1762,7 @@ Proof.
 apply: (iffP idP) => [dvFm i Pi | dvFm].
   by rewrite (bigD1 i) // dvdn_lcm in dvFm; case/andP: dvFm.
 by elim/big_ind: _ => // p q p_m; rewrite dvdn_lcm p_m.
-Qed. 
+Qed.
 
 Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m :
   P i0 -> m %| F i0 -> m %| \big[lcmn/1%N]_(i | P i) F i.
@@ -1777,7 +1777,7 @@ Proof.
 apply: (iffP idP) => [dvmF i Pi | dvmF].
   by rewrite (bigD1 i) // dvdn_gcd in dvmF; case/andP: dvmF.
 by elim/big_ind: _ => // p q m_p; rewrite dvdn_gcd m_p.
-Qed. 
+Qed.
 
 Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
   P i0 -> F i0 %| m -> \big[gcdn/0]_(i | P i) F i %| m.
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index e42b1fd..98ee64e 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -273,7 +273,7 @@ Qed.
 
 Lemma triangular_sum n : \sum_(0 <= i < n) i = 'C(n, 2).
 Proof.
-elim: n => [|n IHn]; first by rewrite big_geq. 
+elim: n => [|n IHn]; first by rewrite big_geq.
 by rewrite big_nat_recr // IHn binS bin1.
 Qed.
 
@@ -307,7 +307,7 @@ suffices{k i} fxx k i: f k.+1 i.+1 = f k i.+1 + f k i.
   by rewrite big_ord_recl big_ord0 addn0 !bin0 muln1.
 rewrite {}/f big_ord_recl (big_ord_recl (i.+1)) !bin0 !mul1n.
 rewrite -addnA -big_split /=; congr (_ + _).
-by apply: eq_bigr => j _ ; rewrite -mulnDl.
+by apply: eq_bigr => j _; rewrite -mulnDl.
 Qed.
 
 Lemma subn_exp m n k :
@@ -504,7 +504,7 @@ Qed.
 Lemma card_partial_ord_partitions m n :
   #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i <= n]| = 'C(m + n, m).
 Proof.
-symmetry; set In1 := 'I_n.+1; pose x0 : In1 := ord0. 
+symmetry; set In1 := 'I_n.+1; pose x0 : In1 := ord0.
 pose add_mn (i j : In1) : In1 := inord (i + j).
 pose f_add (t : m.-tuple In1) := [tuple of scanl add_mn x0 t].
 rewrite -card_sorted_tuples -!sum1dep_card (reindex f_add) /=.
@@ -535,7 +535,7 @@ Qed.
 Lemma card_ord_partitions m n :
   #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
 Proof.
-symmetry; set In1 := 'I_n.+1; pose x0 : In1 := ord0. 
+symmetry; set In1 := 'I_n.+1; pose x0 : In1 := ord0.
 pose f_add (t : m.-tuple In1) := [tuple of sub_ord (\sum_(x <- t) x) :: t].
 rewrite -card_partial_ord_partitions -!sum1dep_card (reindex f_add) /=.
   by apply: eq_bigl => t; rewrite big_cons /= addnC (sameP maxn_idPr eqP) maxnE.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 723946d..4172430 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -200,7 +200,7 @@ rewrite leq_subLR addnA; apply: leq_trans (leq_divDl _ _ _).
 by rewrite -maxnE leq_div2r ?leq_maxr.
 Qed.
 
-Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p. 
+Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p.
 Proof.
 case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //.
 rewrite {2}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //.
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index e00ddef..43ba42a 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -207,7 +207,7 @@ Lemma pffun_onP y D R f :
           (f \in pffun_on_mem y (mem D) (mem R)).
 Proof.
 apply: (iffP (pfamilyP y D (fun _ => R) f)) => [] [-> f_fam]; split=> //.
-  by move=>  _ /imageP[x Ax ->]; apply: f_fam.
+  by move=> _ /imageP[x Ax ->]; apply: f_fam.
 by move=> x Ax; apply: f_fam; apply/imageP; exists x.
 Qed.
 
@@ -267,7 +267,7 @@ apply/imageP/andP=> [[f0 /familyP/=Ff0] [{f}-> ->]| [Fy /familyP/=Ff]].
   split; first by have:= Ff0 x0; rewrite /= mem_head.
   apply/familyP=> x; have:= Ff0 x; rewrite ffunE inE /=.
   by case: eqP => //= -> _; rewrite ifN ?inE.
-exists (g (y, f)). 
+exists (g (y, f)).
   by apply/familyP=> x; have:= Ff x; rewrite ffunE /= inE; case: eqP => // ->.
 congr (_, _); last apply/ffunP=> x; do !rewrite ffunE /= ?eqxx //.
 by case: eqP => // ->{x}; apply/eqP; have:= Ff x0; rewrite ifN.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index a9899b7..dc964b5 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -746,7 +746,7 @@ Lemma cardsU A B : #|A :|: B| = (#|A| + #|B| - #|A :&: B|)%N.
 Proof. by rewrite -cardsUI addnK. Qed.
 
 Lemma cardsI A B : #|A :&: B| = (#|A| + #|B| - #|A :|: B|)%N.
-Proof. by rewrite  -cardsUI addKn. Qed.
+Proof. by rewrite -cardsUI addKn. Qed.
 
 Lemma cardsT : #|[set: T]| = #|T|.
 Proof. by rewrite cardsE. Qed.
@@ -1969,7 +1969,7 @@ Qed.
 Lemma pblock_equivalence_partition :
   {in D &, forall x y, (y \in pblock P x) = R x y}.
 Proof.
-have [_ tiP _] := and3P equivalence_partitionP. 
+have [_ tiP _] := and3P equivalence_partitionP.
 by move=> x y Dx Dy; rewrite /= (def_pblock tiP (PPx Dx) (Pxx Dx)) inE Dy.
 Qed.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 1171fcb..719a267 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -506,7 +506,7 @@ Lemma cardE A : #|A| = size (enum A).
 Proof. by rewrite unlock. Qed.
 
 Lemma eq_card A B : A =i B -> #|A| = #|B|.
-Proof. by move=>eqAB; rewrite !cardE (eq_enum eqAB). Qed.
+Proof. by move=> eqAB; rewrite !cardE (eq_enum eqAB). Qed.
 
 Lemma eq_card_trans A B n : #|A| = n -> B =i A -> #|B| = n.
 Proof. by move <-; apply: eq_card. Qed.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 5533832..0aafc34 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -140,7 +140,7 @@ Local Notation "\pi" := (pi_phant (Phant qT)).
 Definition repr_of := quot_repr (quot_class qT).
 
 Lemma repr_ofK : cancel repr_of \pi.
-Proof. by rewrite /pi_phant /repr_of /=; case:qT=> [? []]. Qed.
+Proof. by rewrite /pi_phant /repr_of /=; case: qT=> [? []]. Qed.
 
 Definition QuotType_clone (Q : Type) qT cT 
   of phant_id (quot_class qT) cT := @QuotTypePack Q cT Q.
@@ -487,7 +487,7 @@ Lemma equiv_sym : symmetric e. Proof. by case: e => [] ? []. Qed.
 Lemma equiv_trans : transitive e. Proof. by case: e => [] ? []. Qed.
 
 Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
-Proof. by move=> x y z;  move/eqP->; move/eqP->. Qed.
+Proof. by move=> x y z; move/eqP->; move/eqP->. Qed.
 
 Lemma equiv_ltrans: left_transitive e.
 Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
@@ -567,7 +567,7 @@ Qed.
 
 Canonical encoded_equiv_equiv_rel := EquivRelPack encoded_equiv_is_equiv.
 
-Lemma encoded_equivP x : e' (DE (ED x)) x. 
+Lemma encoded_equivP x : e' (DE (ED x)) x.
 Proof. by rewrite /encoded_equiv /= encModEquivP. Qed.
 
 End EncodingModuloEquiv.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index f5eb77b..6ab7926 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -213,7 +213,7 @@ Lemma next_nth p x :
                if p is y :: p' then nth y p' (index x p) else x
              else x.
 Proof.
-case: p => //= y0 p. 
+case: p => //= y0 p.
 elim: p {2 3 5}y0 => [|y' p IHp] y /=; rewrite (eq_sym y) inE;
   by case: ifP => // _; apply: IHp.
 Qed.
@@ -542,7 +542,7 @@ have: perm_eq (catss ss ++ s) (merge_sort_pop s ss).
   by rewrite perm_catC catA perm_catC perm_cat2l -perm_merge.
 case: s => // x1 [//|x2 s _]; move/ltnW; move/IHn=> {n IHn}IHs.
 rewrite -{IHs}(perm_eqrP (IHs _)) ifE; set s1 := if_expr _ _ _.
-rewrite (catA _ [::_;_] s) {s}perm_cat2r.
+rewrite (catA _ [::_; _] s) {s}perm_cat2r.
 apply: (@perm_eq_trans _ (catss ss ++ s1)).
   by rewrite perm_cat2l /s1 -ifE; case: ifP; rewrite // (perm_catC [::_]).
 elim: ss {x1 x2}s1 => /= [|s2 ss IHss] s1; first by rewrite cats0.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 41243ea..9494353 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -998,7 +998,7 @@ apply/eqP; rewrite eqn_dvd dvdn_lcm !partn_dvd ?dvdn_lcml ?dvdn_lcmr //.
 rewrite -(dvdn_pmul2r (part_gt0 pi^' (lcmn m n))) partnC // dvdn_lcm !andbT.
 rewrite -{1}(partnC pi m_gt0) andbC -{1}(partnC pi n_gt0).
 by rewrite !dvdn_mul ?partn_dvd ?dvdn_lcml ?dvdn_lcmr.
-Qed. 
+Qed.
 
 Lemma partn_gcd pi m n : m > 0 -> n > 0 -> (gcdn m n)`_pi = gcdn m`_pi n`_pi.
 Proof.
@@ -1007,7 +1007,7 @@ apply/eqP; rewrite eqn_dvd dvdn_gcd !partn_dvd ?dvdn_gcdl ?dvdn_gcdr //=.
 rewrite -(dvdn_pmul2r (part_gt0 pi^' (gcdn m n))) partnC // dvdn_gcd.
 rewrite -{3}(partnC pi m_gt0) andbC -{3}(partnC pi n_gt0).
 by rewrite !dvdn_mul ?partn_dvd ?dvdn_gcdl ?dvdn_gcdr.
-Qed. 
+Qed.
 
 Lemma partn_biglcm (I : finType) (P : pred I) F pi :
     (forall i, P i -> F i > 0) ->
@@ -1313,7 +1313,7 @@ move=> n_gt0; wlog le_b_a: a b / b <= a.
   move=> IH; case: (leqP b a) => [|/ltnW] /IH {IH}// IH.
   by rewrite eq_sym; apply: (iffP IH) => eqab p; move/eqab.
 rewrite eqn_mod_dvd //; apply: (iffP (dvdn_partP _ n_gt0)) => eqab p /eqab;
-  by rewrite -eqn_mod_dvd // => /eqP.   
+  by rewrite -eqn_mod_dvd // => /eqP.
 Qed.
 
 (* The Euler totient function *)
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8c21ae4..1c16140 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -441,12 +441,14 @@ CoInductive eqn0_xor_gt0 n : bool -> bool -> Set :=
 Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
 Proof. by case: n; constructor. Qed.
 
-CoInductive compare_nat m n : bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+CoInductive compare_nat m n :
+   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | CompareNatLt of m < n : compare_nat m n true false true false false false
   | CompareNatGt of m > n : compare_nat m n false true false true false false
   | CompareNatEq of m = n : compare_nat m n true true false false true true.
 
-Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n).
+Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n)
+                                   (n < m) (n == m) (m == n).
 Proof.
 rewrite !ltn_neqAle [_ == m]eq_sym; case: ltnP => [mn|].
   by rewrite ltnW // gtn_eqF //; constructor.