Merge pull request #484 from CohenCyril/ord1

Putting `ord1` in `fintype.v`

4 files changed, 10 insertions, 4 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0a59193..439515b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -160,6 +160,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   variant which does not require an `eqType` is currently named
   `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the
   next release.
+- Added lemma `ord1` in `fintype`, it is the same as `zmodp.ord1`,
+  except `fintype.ord1` does not rely on `'I_n` zmodType structure.
+
 
 - in `order.v`, `\join^d_` and `\meet^d_` notations are now properly specialized
   for `dual_display`.
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 4d92e26..015d971 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -181,8 +181,10 @@ Arguments Zp1 {p'}.
 Arguments inZp {p'} i.
 Arguments valZpK {p'} x.
 
+(* We redefine fintype.ord1 to specialize it with 0 instead of ord0 *)
+(* since 'I_n is now canonically a zmodType  *)
 Lemma ord1 : all_equal_to (0 : 'I_1).
-Proof. by case=> [[] // ?]; apply: val_inj. Qed.
+Proof. exact: ord1. Qed.
 
 Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1).
 Proof. exact: val_inj. Qed.
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.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 3472a1d..f4f34a4 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -2220,6 +2220,9 @@ Arguments sub_ord {n'}.
 Arguments sub_ordK {n'}.
 Arguments inord_val {n'}.
 
+Lemma ord1 : all_equal_to (ord0 : 'I_1).
+Proof. by case=> [[] // ?]; apply: val_inj. Qed.
+
 (* Product of two fintypes which is a fintype *)
 Section ProdFinType.