Merge pull request #153 from arthuraa/finperm

Add a theory of finite permutations.

Author: CohenCyril

.github/workflows/docker-action.yml

@@ -18,10 +18,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
-          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.1'

CHANGELOG_UNRELEASED.md

@@ -7,6 +7,8 @@
 - in `finmap.v`:
   + lemma `card_fset_sum1`
 
+- Added a theory of finite permutations in `finperm.v`
+
 ### Changed
 
 ### Renamed

_CoqProject

@@ -1,5 +1,6 @@
 finmap.v
 multiset.v
+finperm.v
 
 -R . mathcomp.finmap
 -arg -w -arg -projection-no-head-constant