diff options
| author | Cyril Cohen | 2020-09-01 15:44:13 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 19:59:28 +0200 |
| commit | fbeec199e65fe7e9fd96ddd74e31aa0461c22927 (patch) | |
| tree | bff3b089214e20c21a63b053670793a7bf44fe91 /mathcomp/ssreflect/fintype.v | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
Lemmas reindex_omap and bigD1_ord
+ eq_liftF and lift_eqF
+ proof simplificaions
Diffstat (limited to 'mathcomp/ssreflect/fintype.v')
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 88d0f92..3472a1d 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2074,6 +2074,12 @@ Qed. Lemma neq_lift n (h : 'I_n) i : h != lift h i. Proof. exact: neq_bump. Qed. +Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false. +Proof. exact/negbTE/neq_lift. Qed. + +Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false. +Proof. by rewrite eq_sym eq_liftF. Qed. + Lemma unlift_none n (h : 'I_n) : unlift h h = None. Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed. |