Merge pull request #336 from CohenCyril/clean_require

Cleaning Require and Require Imports

19 files changed, 80 insertions, 143 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 16ce432..ad12189 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1,14 +1,10 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype.
-From mathcomp
-Require Import finfun bigop finset prime binomial fingroup morphism perm.
-From mathcomp
-Require Import automorphism action quotient gfunctor gproduct ssralg finalg.
-From mathcomp
-Require Import zmodp cyclic pgroup gseries nilpotent sylow.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div fintype finfun bigop finset prime binomial.
+From mathcomp Require Import fingroup morphism perm automorphism action.
+From mathcomp Require Import quotient gfunctor gproduct ssralg finalg zmodp.
+From mathcomp Require Import cyclic pgroup gseries nilpotent sylow.
 
 (******************************************************************************)
 (* Constructions based on abelian groups and their structure, with some       *)
diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index b0e4c22..d6ada5f 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div fintype tuple.
-From mathcomp
-Require Import tuple bigop prime finset fingroup morphism perm automorphism.
-From mathcomp
-Require Import quotient action cyclic pgroup gseries sylow primitive_action.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype tuple tuple bigop prime finset fingroup.
+From mathcomp Require Import morphism perm automorphism quotient action cyclic.
+From mathcomp Require Import pgroup gseries sylow primitive_action.
 
 (******************************************************************************)
 (*  Definitions of the symmetric and alternate groups, and some properties.   *)
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index f5f3719..b5d34a5 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -1,10 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import tuple finfun bigop finset fingroup action perm primitive_action.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple finfun bigop finset fingroup.
+From mathcomp Require Import action perm primitive_action.
 
 (*   Application of the Burside formula to count the number of distinct       *)
 (* colorings of the vertices of a square and a cube.                          *)
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index e2c6f48..615e0ac 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
-From mathcomp
-Require Import finset fingroup morphism perm automorphism quotient action.
-From mathcomp
-Require Import gproduct gfunctor cyclic.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype bigop finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient action gproduct gfunctor.
+From mathcomp Require Import cyclic.
 
 (******************************************************************************)
 (* Definition of the center of a group and of external central products:      *)
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index 7895116..a1ffb65 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -1,10 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat fintype bigop finset.
-From mathcomp
-Require Import binomial fingroup morphism automorphism quotient gfunctor.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype.
+From mathcomp Require Import bigop finset binomial fingroup morphism.
+From mathcomp Require Import automorphism quotient gfunctor.
 
 (******************************************************************************)
 (*   This files contains the proofs of several key properties of commutators, *)
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index e370a7e..e6d3afb 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
-From mathcomp
-Require Import prime finset fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import gproduct ssralg finalg zmodp poly.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype bigop prime finset fingroup morphism.
+From mathcomp Require Import perm automorphism quotient gproduct ssralg.
+From mathcomp Require Import finalg zmodp poly.
 
 (******************************************************************************)
 (*  Properties of cyclic groups.                                              *)
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v
index 2c7f6c3..aa3ebed 100644
--- a/mathcomp/solvable/extraspecial.v
+++ b/mathcomp/solvable/extraspecial.v
@@ -1,16 +1,12 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import bigop finset prime binomial fingroup morphism perm automorphism.
-From mathcomp
-Require Import presentation quotient action commutator gproduct gfunctor.
-From mathcomp
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
-From mathcomp
-Require Import nilpotent sylow abelian finmodule matrix maximal extremal.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype bigop finset prime binomial.
+From mathcomp Require Import fingroup morphism perm automorphism presentation.
+From mathcomp Require Import quotient action commutator gproduct gfunctor.
+From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries.
+From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal.
+From mathcomp Require Import extremal.
 
 (******************************************************************************)
 (* This file contains the fine structure thorems for extraspecial p-groups.   *)
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index a51fe9c..65c186a 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -1,16 +1,11 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import bigop finset prime binomial fingroup morphism perm automorphism.
-From mathcomp
-Require Import presentation quotient action commutator gproduct gfunctor.
-From mathcomp
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
-From mathcomp
-Require Import nilpotent sylow abelian finmodule matrix maximal.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype bigop finset prime binomial.
+From mathcomp Require Import fingroup morphism perm automorphism presentation.
+From mathcomp Require Import quotient action commutator gproduct gfunctor.
+From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries.
+From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal.
 
 (******************************************************************************)
 (*    This file contains the definition and properties of extremal p-groups;  *)
diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index 9afe26a..05c070e 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
-From mathcomp
-Require Import fintype bigop ssralg finset fingroup morphism perm.
-From mathcomp
-Require Import finalg action gproduct commutator cyclic.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype bigop ssralg finset fingroup.
+From mathcomp Require Import morphism perm finalg action gproduct commutator.
+From mathcomp Require Import cyclic.
 
 (******************************************************************************)
 (*  This file regroups constructions and results that are based on the most   *)
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index 01ba8f3..71b8b34 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat div fintype bigop prime.
-From mathcomp
-Require Import finset fingroup morphism perm action quotient gproduct.
-From mathcomp
-Require Import cyclic center pgroup nilpotent sylow hall abelian.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div.
+From mathcomp Require Import fintype bigop prime finset fingroup morphism.
+From mathcomp Require Import perm action quotient gproduct cyclic center.
+From mathcomp Require Import pgroup nilpotent sylow hall abelian.
 
 (******************************************************************************)
 (*  Definition of Frobenius groups, some basic results, and the Frobenius     *)
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v
index fc8385d..31ffded 100644
--- a/mathcomp/solvable/gfunctor.v
+++ b/mathcomp/solvable/gfunctor.v
@@ -1,10 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat fintype bigop finset.
-From mathcomp
-Require Import fingroup morphism automorphism quotient gproduct.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype.
+From mathcomp Require Import bigop finset fingroup morphism automorphism.
+From mathcomp Require Import quotient gproduct.
 
 (******************************************************************************)
 (*   This file provides basic interfaces for the notion of "generic"          *)
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index 3e99bfb..28ca208 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path fintype bigop.
-From mathcomp
-Require Import finset fingroup morphism automorphism quotient action.
-From mathcomp
-Require Import commutator center.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import fintype bigop finset fingroup morphism.
+From mathcomp Require Import automorphism quotient action commutator center.
+
 (******************************************************************************)
 (*           H <|<| G   <=> H is subnormal in G, i.e., H <| ... <| G.         *)
 (* invariant_factor A H G <=> A normalises both H and G, and H <| G.          *)
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index 68c2863..43e429f 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -1,14 +1,10 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div fintype finset.
-From mathcomp
-Require Import prime fingroup morphism automorphism quotient action gproduct.
-From mathcomp
-Require Import gfunctor commutator center pgroup finmodule nilpotent sylow.
-From mathcomp
-Require Import abelian maximal.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype finset prime fingroup morphism.
+From mathcomp Require Import automorphism quotient action gproduct gfunctor.
+From mathcomp Require Import commutator center pgroup finmodule nilpotent.
+From mathcomp Require Import sylow abelian maximal.
 
 (*****************************************************************************)
 (*  In this files we prove the Schur-Zassenhaus splitting and transitivity   *)
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index bda66bd..1a32bce 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -1,12 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype.
-From mathcomp
-Require Import bigop finset fingroup morphism automorphism quotient action.
-From mathcomp
-Require Import gseries.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import choice fintype bigop finset fingroup morphism.
+From mathcomp Require Import automorphism quotient action gseries.
 
 (******************************************************************************)
 (* This files establishes Jordan-Holder theorems for finite groups. These     *)
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 781abbe..f3d79fc 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1,16 +1,11 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype.
-From mathcomp
-Require Import finfun bigop finset prime binomial fingroup morphism perm.
-From mathcomp
-Require Import automorphism quotient action commutator gproduct gfunctor.
-From mathcomp
-Require Import ssralg finalg zmodp cyclic pgroup center gseries.
-From mathcomp
-Require Import nilpotent sylow abelian finmodule.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
+From mathcomp Require Import div fintype finfun bigop finset prime binomial.
+From mathcomp Require Import fingroup morphism perm automorphism quotient.
+From mathcomp Require Import action commutator gproduct gfunctor ssralg.
+From mathcomp Require Import finalg zmodp cyclic pgroup center gseries.
+From mathcomp Require Import nilpotent sylow abelian finmodule.
 
 (******************************************************************************)
 (*   This file establishes basic properties of several important classes of   *)
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index aee3113..f0448d7 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path fintype div.
-From mathcomp
-Require Import bigop prime finset fingroup morphism automorphism quotient.
-From mathcomp
-Require Import commutator gproduct gfunctor center gseries cyclic.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import fintype div bigop prime finset fingroup morphism.
+From mathcomp Require Import automorphism quotient commutator gproduct.
+From mathcomp Require Import gfunctor center gseries cyclic.
 
 (******************************************************************************)
 (*   This file defines nilpotent and solvable groups, and give some of their  *)
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index d62154f..5c572b7 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div.
-From mathcomp
-Require Import fintype bigop finset prime fingroup morphism.
-From mathcomp
-Require Import gfunctor automorphism quotient action gproduct cyclic.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype bigop finset prime fingroup morphism.
+From mathcomp Require Import gfunctor automorphism quotient action gproduct.
+From mathcomp Require Import cyclic.
 
 (******************************************************************************)
 (* Standard group notions and constructions based on the prime decomposition  *)
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index 73e397d..e6016e8 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -1,12 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat.
-From mathcomp
-Require Import div seq fintype tuple finset.
-From mathcomp
-Require Import fingroup action gseries.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+From mathcomp Require Import div seq fintype tuple finset.
+From mathcomp Require Import fingroup action gseries.
 
 (******************************************************************************)
 (* n-transitive and primitive actions:                                        *)
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index a428c0d..2a46564 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div fintype prime.
-From mathcomp
-Require Import bigop finset fingroup morphism automorphism quotient action.
-From mathcomp
-Require Import cyclic gproduct gfunctor commutator pgroup center nilpotent.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
+From mathcomp Require Import fintype prime bigop finset fingroup morphism.
+From mathcomp Require Import automorphism quotient action cyclic gproduct.
+From mathcomp Require Import gfunctor commutator pgroup center nilpotent.
 
 (******************************************************************************)
 (*   The Sylow theorem and its consequences, including the Frattini argument, *)