From 4241f07301e8d84186ae2c80d5c32118a90f6847 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 10 Apr 2020 11:45:05 +0200
Subject: Putting ord1 in fintype

ord1 is in zmodp, but it does not really require the zmodType structure of 'I_n to be stated and proven if we state it with ord0. We still keep the variant in zmodp with 0 instead of ord0 (for readability purposes).
---
 mathcomp/fingroup/perm.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'mathcomp/fingroup')

diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 0c02f3b..d0ba321 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -638,9 +638,7 @@ Lemma permS0 : all_equal_to (1 : 'S_0).
 Proof. by move=> g; apply/permP; case. Qed.
 
 Lemma permS1 : all_equal_to (1 : 'S_1).
-Proof.
-by move=> g; apply/permP => i; apply: val_inj; do ![case: (X in val X); case].
-Qed.
+Proof. by move=> g; apply/permP => i; rewrite !ord1. Qed.
 
 Section CastSn.
 
-- 
cgit v1.2.3