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

---
 mathcomp/fingroup/perm.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'mathcomp/fingroup')

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