From 486e08591c443093cdb602de7f603f84df72be42 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 6 Apr 2020 03:04:22 +0900
Subject: Adding `permS01`

---
 CHANGELOG_UNRELEASED.md  | 1 +
 mathcomp/fingroup/perm.v | 3 +++
 2 files changed, 4 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d8bd318..86c920b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -250,6 +250,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
    Its name will become `prodrMn` in the next release when this name will become available (cf. Renamed section)
 
 - in `polydiv.v`, new lemma `dvdpNl`.
+- in `perm.v` new lemma `permS01`.
 
 ### Changed
 
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index ebd4230..5775e34 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -640,6 +640,9 @@ Proof. by move=> g; apply/permP; case. Qed.
 Lemma permS1 : all_equal_to (1 : 'S_1).
 Proof. by move=> g; apply/permP => i; rewrite !ord1. Qed.
 
+Lemma permS01 n : n <= 1 -> all_equal_to (1 : 'S_n).
+Proof. by case: n => [|[|]//=] _ g; rewrite (permS0, permS1). Qed.
+
 Section CastSn.
 
 Definition cast_perm m n (eq_mn : m = n) (s : 'S_m) :=
-- 
cgit v1.2.3