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/ssreflect/fintype.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'mathcomp/ssreflect')

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.
 
-- 
cgit v1.2.3