From fbeec199e65fe7e9fd96ddd74e31aa0461c22927 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 1 Sep 2020 15:44:13 +0200
Subject: Lemmas reindex_omap and bigD1_ord

+ eq_liftF and lift_eqF
+ proof simplificaions
---
 mathcomp/field/algnum.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 997255b..821a21e 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -150,8 +150,8 @@ Lemma mem_Crat_span s : {subset s <= Crat_span s}.
 Proof.
 move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs.
 apply/Crat_spanP; exists [ffun i => (i == i0)%:R].
-rewrite (bigD1 i0) //= ffunE eqxx // rmorph1 mul1r.
-by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl => /negbTE->.
+rewrite (bigD1_ord i0) //= ffunE eqxx // rmorph1 mul1r.
+by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl lift_eqF.
 Qed.
 
 Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
-- 
cgit v1.2.3