From 6e40eec5f5697499503824820e2e8b5a42fb411e Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 29 Aug 2018 00:18:30 +0200
Subject: [PATCH 1/9] monalg for finmap v1.1

---
 src/monalg.v  | 192 +++++++++++++++++++++++++++-----------------------
 src/xfinmap.v |  58 +--------------
 2 files changed, 105 insertions(+), 145 deletions(-)

diff --git a/src/monalg.v b/src/monalg.v
index 98f7b5e..0544ee0 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -598,18 +598,19 @@ Definition monalgUE :=
 
 (* -------------------------------------------------------------------- *)
 Lemma monalgEw (g : {malg G[K]}) (domg : {fset K}) : msupp g `<=` domg ->
-  g = \sum_(k : domg) << g@_(val k) *g val k >>.
-Proof.
-move=> le_gd; apply/eqP/malgP=> k /=; case: msuppP=> [kg|k_notin_g].
-  rewrite raddf_sum /= (bigD1 (fincl le_gd (FSetSub kg))) //=.
-  rewrite mcoeffUU big1 ?addr0 //; case=> [k' k'_in_g] /=.
-  by rewrite eqE /= mcoeffU => /negbTE ->.
-rewrite raddf_sum /= big1 //; case=> [k' k'g] _ /=.
+  g = \sum_(k <- domg) << g@_k *g k >>.
+Proof.
+move/fsubsetP=> le_gd; apply/eqP/malgP=> k /=; case: msuppP=> [kg|k_notin_g].
+  rewrite raddf_sum /= (big_fsetD1 k) //=; last by apply: le_gd.
+  rewrite mcoeffUU ?addr0 // big1_fset ?addr0 // => k'.
+  rewrite in_fsetD1 => /andP [/negbTE k_ne_k' _ _].
+  by rewrite mcoeffU k_ne_k'.
+rewrite raddf_sum /= big1_fset // => k' _ _.
 by rewrite mcoeffU; case: eqP k_notin_g=> // <- /mcoeff_outdom ->.
 Qed.
 
 Lemma monalgE (g : {malg G[K]}) :
-  g = \sum_(k : msupp g) << g@_(val k) *g val k >>.
+  g = \sum_(k <- msupp g) << g@_k *g k >>.
 Proof. by apply/monalgEw/fsubset_refl. Qed.
 End MAlgZModTheory.
 
@@ -677,7 +678,7 @@ Implicit Types c x y z : R.
 Implicit Types k l     : K.
 
 Definition fgscale c g : {malg R[K]} :=
-  \sum_(k : msupp g) << c * g@_(val k) *g val k >>.
+  \sum_(k <- msupp g) << c * g@_k *g k >>.
 
 Local Notation "c *:g g" := (fgscale c g)
   (at level 40, left associativity).
@@ -778,11 +779,11 @@ Local Notation "g1 *M_[ k1 , k2 ] g2" :=
   (at level 40, no associativity, format "g1  *M_[ k1 ,  k2 ]  g2").
 
 Local Notation "g1 *gM_[ k2 ] g2" :=
-  (\sum_(k1 : msupp g1) g1 *M_[val k1, k2] g2)
+  (\sum_(k1 <- msupp g1) g1 *M_[k1, k2] g2)
   (at level 40, no associativity, only parsing).
 
 Local Notation "g1 *Mg_[ k1 ] g2" :=
-  (\sum_(k2 : msupp g2) g1 *M_[k1, val k2] g2)
+  (\sum_(k2 <- msupp g2) g1 *M_[k1, k2] g2)
   (at level 40, no associativity, only parsing).
 
 Local Notation fg1mull_r g1 g2 k2 :=
@@ -795,40 +796,41 @@ Local Notation fg1mull := (fg1mull_r _ _ _) (only parsing).
 Local Notation fg1mulr := (fg1mulr_r _ _ _) (only parsing).
 
 Definition fgmul g1 g2 : {malg R[K]} :=
-  \sum_(k1 : msupp g1) \sum_(k2 : msupp g2)
-    g1 *M_[val k1, val k2] g2.
+  \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2)
+    g1 *M_[k1, k2] g2.
 
 Lemma fgmull g1 g2 :
-  fgmul g1 g2 = \sum_(k1 : msupp g1) \sum_(k2 : msupp g2)
-    g1 *M_[val k1, val k2] g2.
+  fgmul g1 g2 = \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2)
+    g1 *M_[k1, k2] g2.
 Proof. by []. Qed.
 
 Lemma fgmulr g1 g2 :
-  fgmul g1 g2 = \sum_(k2 : msupp g2) \sum_(k1 : msupp g1)
-    g1 *M_[val k1, val k2] g2.
+  fgmul g1 g2 = \sum_(k2 <- msupp g2) \sum_(k1 <- msupp g1)
+    g1 *M_[k1, k2] g2.
 Proof. by rewrite fgmull exchange_big. Qed.
 
-Let fg1mulzg g1 g2 k1 k2 : k1 \notin msupp g1 -> 
+Let fg1mulzg g1 g2 k1 k2 : k1 \notin msupp g1 ->
   << g1@_k1 * g2@_k2 *g (k1 * k2)%M >> = 0.
 Proof. by move/mcoeff_outdom=> ->; rewrite mul0r monalgU0. Qed.
 
-Let fg1mulgz g1 g2 k1 k2 : k2 \notin msupp g2 -> 
+Let fg1mulgz g1 g2 k1 k2 : k2 \notin msupp g2 ->
   << g1@_k1 * g2@_k2 *g (k1 * k2)%M >> = 0.
 Proof. by move/mcoeff_outdom=> ->; rewrite mulr0 monalgU0. Qed.
 
+(* big_fset_incl has (op : com_law idx) as first non automatic argument *)
 Lemma fgmullw (d1 d2 : {fset K}) g1 g2 :
   msupp g1 `<=` d1 -> msupp g2 `<=` d2 -> fgmul g1 g2 =
-    \sum_(k1 : d1) \sum_(k2 : d2) g1 *M_[val k1, val k2] g2.
+    \sum_(k1 <- d1) \sum_(k2 <- d2) g1 *M_[k1, k2] g2.
 Proof.
 move=> le_d1 le_d2; pose F k1 := g1 *Mg_[k1] g2.
-rewrite fgmull (big_fset_incl F le_d1) {}/F /=; last first.
+rewrite fgmull (big_fset_incl _ le_d1) {}/F /=; last first.
   by move=> k _ /fg1mulzg ?; rewrite big1.
-apply/eq_bigr=> k1 _; rewrite (big_fset_incl fg1mulr le_d2) //.
+apply/eq_bigr=> k1 _; rewrite (big_fset_incl _ le_d2) //.
 by move=> x _ /fg1mulgz.
 Qed.
 
 Lemma fgmulrw (d1 d2 : {fset K}) g1 g2 : msupp g1 `<=` d1 -> msupp g2 `<=` d2
-  -> fgmul g1 g2 = \sum_(k2 : d2) \sum_(k1 : d1) g1 *M_[val k1, val k2] g2.
+  -> fgmul g1 g2 = \sum_(k2 <- d2) \sum_(k1 <- d1) g1 *M_[k1, k2] g2.
 Proof. by move=> le_d1 le_d2; rewrite (fgmullw le_d1 le_d2) exchange_big. Qed.
 
 Definition fgmullwl (d1 : {fset K}) {g1 g2} (le : msupp g1 `<=` d1) :=
@@ -837,10 +839,10 @@ Definition fgmullwl (d1 : {fset K}) {g1 g2} (le : msupp g1 `<=` d1) :=
 Definition fgmulrwl (d2 : {fset K}) {g1 g2} (le : msupp g2 `<=` d2) :=
   @fgmulrw _ _ g1 g2 (fsubset_refl _) le.
 
-Lemma fgmulElw (d1 d2 : {fset K}) g1 g2 k : 
+Lemma fgmulElw (d1 d2 : {fset K}) g1 g2 k :
     msupp g1 `<=` d1 -> msupp g2 `<=` d2
-  -> (fgmul g1 g2)@_k = \sum_(k1 : d1) \sum_(k2 : d2)
-        (g1@_(val k1) * g2@_(val k2)) *+ ((val k1 * val k2)%M == k).
+  -> (fgmul g1 g2)@_k = \sum_(k1 <- d1) \sum_(k2 <- d2)
+        (g1@_k1 * g2@_k2) *+ ((k1 * k2)%M == k).
 Proof.
 move=> le1 le2; rewrite (fgmullw le1 le2) raddf_sum /=.
 apply/eq_bigr=> k1 _; rewrite raddf_sum /=; apply/eq_bigr=> k2 _.
@@ -848,39 +850,39 @@ by rewrite mcoeffsE.
 Qed.
 
 Lemma fgmulErw (d1 d2 : {fset K}) g1 g2 k : msupp g1 `<=` d1 -> msupp g2 `<=` d2
-  -> (fgmul g1 g2)@_k = \sum_(k2 : d2) \sum_(k1 : d1)
-        (g1@_(val k1) * g2@_(val k2)) *+ ((val k1 * val k2)%M == k).
+  -> (fgmul g1 g2)@_k = \sum_(k2 <- d2) \sum_(k1 <- d1)
+        (g1@_k1 * g2@_k2) *+ ((k1 * k2)%M == k).
 Proof. by move=> le1 le2; rewrite (fgmulElw _ le1 le2); rewrite exchange_big. Qed.
 
 Lemma fgmul0g g : fgmul 0 g = 0.
-Proof. by rewrite fgmull msupp0 big_fset0. Qed.
+Proof. by rewrite fgmull msupp0 big_seq_fset0. Qed.
 
 Lemma fgmulg0 g : fgmul g 0 = 0.
-Proof. by rewrite fgmulr msupp0 big_fset0. Qed.
+Proof. by rewrite fgmulr msupp0 big_seq_fset0. Qed.
 
 Lemma fgmulUg (d : {fset K}) c k g : msupp g `<=` d ->
  fgmul << c *g k >> g =
-   \sum_(k' : d) << c * g@_(val k') *g (k * val k')%M >>.
+   \sum_(k' <- d) << c * g@_k' *g (k * k')%M >>.
 Proof.
-move=> le; rewrite (fgmullw msuppU_le le) big_fset1 /=.
+move=> le; rewrite (fgmullw msuppU_le le) big_seq_fset1 /=.
 by apply/eq_bigr=> /= k' _; rewrite mcoeffUU.
 Qed.
 
 Lemma fgmulgU (d : {fset K}) c k g : msupp g `<=` d ->
  fgmul g << c *g k >> =
-   \sum_(k' : d) << g@_(val k') * c *g (val k' * k)%M >>.
+   \sum_(k' <- d) << g@_k' * c *g (k' * k)%M >>.
 Proof.
-move=> le; rewrite (fgmulrw le msuppU_le) big_fset1 /=.
+move=> le; rewrite (fgmulrw le msuppU_le) big_seq_fset1 /=.
 by apply/eq_bigr=> /= k' _; rewrite mcoeffUU.
 Qed.
 
 Lemma fgmulUU c1 c2 k1 k2 :
   fgmul << c1 *g k1 >> << c2 *g k2 >> = << c1 * c2 *g (k1 * k2)%M >>.
-Proof. by rewrite (fgmullw msuppU_le msuppU_le) !big_fset1 /= !mcoeffUU. Qed.
+Proof. by rewrite (fgmullw msuppU_le msuppU_le) !big_seq_fset1 /= !mcoeffUU. Qed.
 
 Lemma fgmulEl1w (d1 : {fset K}) {g1 g2}  :
   msupp g1 `<=` d1 -> fgmul g1 g2
-    = \sum_(k1 : d1) fgmul << g1@_(val k1) *g val k1 >> g2.
+    = \sum_(k1 <- d1) fgmul << g1@_k1 *g k1 >> g2.
 Proof.
 move=> le; rewrite (fgmullwl le); apply/eq_bigr=> /= k _.
 by rewrite -fgmulUg // fsubset_refl.
@@ -888,7 +890,7 @@ Qed.
 
 Lemma fgmulEr1w (d2 : {fset K}) {g1 g2} :
   msupp g2 `<=` d2 -> fgmul g1 g2
-    = \sum_(k2 : d2) fgmul g1 << g2@_(val k2) *g val k2 >>.
+    = \sum_(k2 <- d2) fgmul g1 << g2@_k2 *g k2 >>.
 Proof.
 move=> le; rewrite (fgmulrwl le); apply/eq_bigr=> /= k _.
 by rewrite -fgmulgU // fsubset_refl.
@@ -919,19 +921,18 @@ Proof. by rewrite mcoeffU1 eq_sym. Qed.
 Lemma fgmulA : associative fgmul.
 Proof.
 move=> g1 g2 g3; pose_big_fset K E.
-  transitivity (\sum_(k1 : E) \sum_(k2 : E) \sum_(k3 : E)
-    << g1@_(val k1) * g2@_(val k2) * g3@_(val k3) *g
-         (val k1 * val k2 * val k3)%M >>).
+  transitivity (\sum_(k1 <- E) \sum_(k2 <- E) \sum_(k3 <- E)
+    << g1@_k1 * g2@_k2 * g3@_k3 *g (k1 * k2 * k3)%M >>).
   + rewrite (@fgmulEl1w E) //; apply/eq_bigr=> /= k1 _.
     rewrite [X in fgmul _ X](@fgmullw E E) //.
-    have /= raddf := raddf_sum (fgmullUg_additive g1@_(val k1) (val k1)).
+    have /= raddf := raddf_sum (fgmullUg_additive g1@_k1 k1).
     rewrite raddf; apply/eq_bigr=> /= k2 _; rewrite raddf.
     by apply/eq_bigr=> /= k3 _; rewrite fgmulUU mulrA mulmA.
   2: by close.
 rewrite [LHS](eq_bigr _ (fun _ _ => exchange_big _ _ _ _ _ _)) /=.
 rewrite exchange_big /=; apply/esym; rewrite (@fgmulEr1w E) //.
 apply/eq_bigr=> /= k3 _; rewrite (@fgmullw E E g1) //.
-have /= raddf := raddf_sum (fgmullgU_additive g3@_(val k3) (val k3)).
+have /= raddf := raddf_sum (fgmullgU_additive g3@_k3 k3).
 rewrite raddf; apply/eq_bigr=> /= k1 _; rewrite raddf.
 by apply/eq_bigr=> /= k2 _; rewrite fgmulUU.
 Qed.
@@ -939,14 +940,14 @@ Qed.
 Lemma fgmul1g : left_id fgone fgmul.
 Proof.
 move=> g; rewrite fgmull; apply/eqP/malgP=> k.
-rewrite msuppU1 big_fset1 [X in _=X@__]monalgE !raddf_sum /=.
+rewrite msuppU1 big_seq_fset1 [X in _=X@__]monalgE !raddf_sum /=.
 by apply/eq_bigr=> kg _; rewrite fgoneE eqxx mul1r mul1m.
 Qed.
 
 Lemma fgmulg1 : right_id fgone fgmul.
 Proof.
 move=> g; rewrite fgmulr; apply/eqP/malgP=> k.
-rewrite msuppU1 big_fset1 [X in _=X@__]monalgE !raddf_sum /=.
+rewrite msuppU1 big_seq_fset1 [X in _=X@__]monalgE !raddf_sum /=.
 by apply/eq_bigr=> kg _; rewrite fgoneE eqxx mulr1 mulm1.
 Qed.
 
@@ -995,38 +996,38 @@ Proof. by []. Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma malgME g1 g2 :
-  g1 * g2 = \sum_(k1 : msupp g1) \sum_(k2 : msupp g2)
-    << g1@_(val k1) * g2@_(val k2) *g (val k1 * val k2)%M >>.
+  g1 * g2 = \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2)
+    << g1@_k1 * g2@_k2 *g (k1 * k2)%M >>.
 Proof. by []. Qed.
 
 Lemma malgMEw (d1 d2 : {fset K}) g1 g2 :
   msupp g1 `<=` d1 -> msupp g2 `<=` d2 ->
-  g1 * g2 = \sum_(k1 : d1) \sum_(k2 : d2)
-    << g1@_(val k1) * g2@_(val k2) *g (val k1 * val k2)%M >>.
+  g1 * g2 = \sum_(k1 <- d1) \sum_(k2 <- d2)
+    << g1@_k1 * g2@_k2 *g (k1 * k2)%M >>.
 Proof. by apply/fgmullw. Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma mcoeffMl g1 g2 k :
-  (g1 * g2)@_k = \sum_(k1 : msupp g1) \sum_(k2 : msupp g2)
-    (g1@_(val k1) * g2@_(val k2)) *+ (val k1 * val k2 == k)%M.
+  (g1 * g2)@_k = \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2)
+    (g1@_k1 * g2@_k2) *+ (k1 * k2 == k)%M.
 Proof. by apply/fgmulElw; apply/fsubset_refl. Qed.
 
 Lemma mcoeffMr g1 g2 k :
-  (g1 * g2)@_k = \sum_(k2 : msupp g2) \sum_(k1 : msupp g1)
-    (g1@_(val k1) * g2@_(val k2)) *+ (val k1 * val k2 == k)%M.
+  (g1 * g2)@_k = \sum_(k2 <- msupp g2) \sum_(k1 <- msupp g1)
+    (g1@_k1 * g2@_k2) *+ (k1 * k2 == k)%M.
 Proof. by apply/fgmulErw; apply/fsubset_refl. Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma mcoeffMlw (d1 d2 : {fset K}) g1 g2 k :
   msupp g1 `<=` d1 -> msupp g2 `<=` d2 ->
-  (g1 * g2)@_k = \sum_(k1 : d1) \sum_(k2 : d2)
-    (g1@_(val k1) * g2@_(val k2)) *+ (val k1 * val k2 == k)%M.
+  (g1 * g2)@_k = \sum_(k1 <- d1) \sum_(k2 <- d2)
+    (g1@_k1 * g2@_k2) *+ (k1 * k2 == k)%M.
 Proof. by apply/fgmulElw. Qed.
 
 Lemma mcoeffMrw (d1 d2 : {fset K}) g1 g2 k :
   msupp g1 `<=` d1 -> msupp g2 `<=` d2 ->
-  (g1 * g2)@_k = \sum_(k2 : d2) \sum_(k1 : d1)
-    (g1@_(val k1) * g2@_(val k2)) *+ (val k1 * val k2 == k)%M.
+  (g1 * g2)@_k = \sum_(k2 <- d2) \sum_(k1 <- d1)
+    (g1@_k1 * g2@_k2) *+ (k1 * k2 == k)%M.
 Proof. by apply/fgmulErw. Qed.
 
 (* -------------------------------------------------------------------- *)
@@ -1042,16 +1043,28 @@ Qed.
 Lemma mcoeffCM c g k : (c%:MP * g)@_k = c * g@_k :> R.
 Proof. by rewrite mul_malgC mcoeffZ. Qed.
 
+(* I don't know here how to avoid going through finType due to the use  *)
+(* of boolean [exists ...]                                              *)
 (* -------------------------------------------------------------------- *)
-Lemma msuppM_le g1 g2 k :
+Lemma msuppM_le_fintype g1 g2 k :
   k \in msupp (g1 * g2) ->
-    exists k1 : msupp g1, exists k2 : msupp g2, k = (val k1 * val k2)%M.
+        exists k1 : msupp g1, exists k2 : msupp g2, k = (val k1 * val k2)%M.
 Proof.
 move=> k_in_g1Mg2; apply/(existsPP (fun _ => exists_eqP)).
 apply/contraLR: k_in_g1Mg2=> hk; rewrite -mcoeff_eq0.
-rewrite mcoeffMl big1 // => /= k1 _; rewrite big1 // => k2 _.
+rewrite mcoeffMl big_seq big1 // => /= k1 Hk1.
+rewrite big_seq big1 // => k2 Hk2.
 case: eqP=> // kE; case/negP: hk; apply/existsP.
-by exists k1; apply/existsP; exists k2; rewrite kE.
+by exists [` Hk1]; apply/existsP; exists [` Hk2]; rewrite kE.
+Qed.
+
+(* -------------------------------------------------------------------- *)
+Lemma msuppM_le g1 g2 k :
+  k \in msupp (g1 * g2) ->
+    exists k1 k2, [/\ k1 \in msupp g1, k2 \in msupp g2 & k = (k1 * k2)%M].
+Proof.
+move/msuppM_le_fintype => [] [k1 Hk1] [] [k2 Hk2] /= Hk.
+by exists k1; exists k2.
 Qed.
 
 (* -------------------------------------------------------------------- *)
@@ -1081,11 +1094,12 @@ Lemma mcoeff1g_is_multiplicative :
   multiplicative (mcoeff 1%M : {malg R[K]} -> R).
 Proof.
 split=> [g1 g2|]; rewrite ?malgCK //; pose_big_fset K E.
-have E1: 1%M \in E by by rewrite -fsub1set.
-rewrite (@malgMEw E E) // (bigD1 (FSetSub E1)) //=. 2: by close.
-rewrite (bigD1 (FSetSub E1)) //= mulm1 2!mcoeffD mcoeffUU.
-rewrite !raddf_sum !big1 ?simpm //= => k; rewrite -val_eqE /= => ne1_k.
-  rewrite raddf_sum big1 ?mcoeff0 //= => k' _; rewrite mcoeffU.
+have E1: 1%M \in E by rewrite -fsub1set.
+rewrite (@malgMEw E E) // (big_fsetD1 1%M) //=. 2: by close.
+rewrite (big_fsetD1 1%M) //= mulm1 2!mcoeffD mcoeffUU.
+rewrite ![\sum_(i <- E `\ 1%M) _]big_seq.
+rewrite !raddf_sum !big1 ?simpm //= => k; rewrite in_fsetD1 => /andP [ne1_k _].
+  rewrite raddf_sum big1 ?mcoeff0 //= => k'; rewrite mcoeffU.
   by case: eqP=> // /eqP /MonomialTheory.unitmP []; rewrite (negbTE ne1_k).
 by rewrite mcoeffU mul1m (negbTE ne1_k).
 Qed.
@@ -1139,10 +1153,10 @@ Section Defs.
 Variables (K : choiceType) (G : zmodType) (S : ringType).
 Variables (f : G -> S) (h : K -> S).
 
-Definition mmap g := \sum_(k : msupp g) (f g@_(val k)) * (h (val k)).
+Definition mmap g := \sum_(k <- msupp g) (f g@_k) * (h k).
 
 Lemma mmapE g :
-  mmap g = \sum_(k : msupp g) (f g@_(val k)) * (h (val k)).
+  mmap g = \sum_(k <- msupp g) (f g@_k) * (h k).
 Proof. by []. Qed.
 End Defs.
 
@@ -1154,16 +1168,16 @@ Variables (K : choiceType) (G : zmodType) (S : ringType).
 Context {f : {additive G -> S}} {h : K -> S}.
 
 Lemma mmapEw (d : {fset K}) g : msupp g `<=` d ->
-  g^[f, h] = \sum_(k : d) (f g@_(val k)) * (h (val k)).
+  g^[f, h] = \sum_(k <- d) (f g@_k) * (h k).
 Proof.
 move=> le; pose F k := (f g@_k) * (h k); rewrite mmapE.
-rewrite (big_fset_incl F le) {}/F //= => k _ /mcoeff_outdom.
+rewrite (big_fset_incl _ le) {}/F //= => k _ /mcoeff_outdom.
 by move=> ->; rewrite raddf0 mul0r.
 Qed.
 
 Lemma mmapU (c : G) (m : K) :
   mmap f h << c *g m >> = (f c) * (h m).
-Proof. by rewrite (mmapEw msuppU_le) big_fset1 mcoeffUU. Qed.
+Proof. by rewrite (mmapEw msuppU_le) big_seq_fset1 mcoeffUU. Qed.
 End BaseTheory.
 
 Section Additive.
@@ -1439,17 +1453,17 @@ Proof. by case: mf=> mf' _ _ h /= mf0; apply/h. Qed.
 Lemma mf_eq0 m : (mf m == 0%N) = (m == 1%M).
 Proof. by apply/eqP/eqP=> [|->]; rewrite ?mf0 // => /mf_eq0I. Qed.
 
-Definition mmeasure g := (\max_(m : msupp g) (mf (val m)).+1)%N.
+Definition mmeasure g := (\max_(m <- msupp g) (mf m).+1)%N.
 
-Lemma mmeasureE g : mmeasure g = (\max_(m : msupp g) (mf (val m)).+1)%N.
+Lemma mmeasureE g : mmeasure g = (\max_(m <- msupp g) (mf m).+1)%N.
 Proof. by []. Qed.
 
 Lemma mmeasure0 : mmeasure 0 = 0%N.
-Proof. by rewrite mmeasureE msupp0 big_fset0. Qed.
+Proof. by rewrite mmeasureE msupp0 big_seq_fset0. Qed.
 
 Lemma mmeasure_mnm_lt g m : m \in msupp g -> (mf m < mmeasure g)%N.
 Proof.
-move=> km; rewrite mmeasureE (bigD1 (FSetSub km)) //=.
+move=> km; rewrite mmeasureE (big_fsetD1 m) //=.
 by rewrite leq_max ltnS leqnn.
 Qed.
 
@@ -1459,16 +1473,18 @@ Proof. by apply/contraTN=> /mmeasure_mnm_lt; rewrite leqNgt ltnS. Qed.
 Lemma mmeasureC c : mmeasure c%:MP = (c != 0%R) :> nat.
 Proof.
 rewrite mmeasureE msuppC; case: (_ == 0)=> /=.
-by rewrite big_fset0. by rewrite big_fset1 mf0.
+by rewrite big_nil. by rewrite big_seq_fset1 mf0.
 Qed.
 
 Lemma mmeasureN g : mmeasure (-g) = mmeasure g.
 Proof. by rewrite mmeasureE msuppN. Qed.
 
+(* Lemmas about max apply only on fintypes and not seq *)
 Lemma mmeasureD_le g1 g2 :
   (mmeasure (g1 + g2) <= maxn (mmeasure g1) (mmeasure g2))%N.
 Proof.
-rewrite {1}mmeasureE; apply/bigmax_leqP=> [[i ki]] _ /=.
+rewrite {1}mmeasureE big_seq_fsetE /=.
+apply/bigmax_leqP=> [[i ki]] _ /=.
 have /fsubsetP /(_ i ki) := (msuppD_le g1 g2); rewrite in_fsetU.
 by rewrite leq_max; case/orP=> /mmeasure_mnm_lt->; rewrite !simpm.
 Qed.
@@ -1486,7 +1502,7 @@ Proof.
 apply/idP/eqP=> [z_g|->]; last by rewrite mmeasure0.
 apply/eqP/malgP=> k; rewrite mcoeff0; apply/contraTeq: z_g.
 rewrite mcoeff_neq0 => kg; rewrite mmeasureE.
-by rewrite (bigD1 (FSetSub kg)) //= -lt0n leq_max.
+by rewrite (big_fsetD1 k) //= -lt0n leq_max.
 Qed.
 
 Lemma malgSpred g : g != 0 -> mmeasure g = (mmeasure g).-1.+1.
@@ -1501,7 +1517,7 @@ Section ComMonomial.
 Section Def.
 Variable (I : choiceType).
 
-Inductive cmonom : predArgType := CMonom of {fsfun _ : I => 0%N}.
+Inductive cmonom : predArgType := CMonom of {fsfun of _ : I => 0%N}.
 
 Definition cmonom_val m := let: CMonom m := m in m.
 Definition cmonom_of (_ : phant I) := cmonom.
@@ -1547,7 +1563,7 @@ Context {I : choiceType}.
 Implicit Types m : {cmonom I}.
 Implicit Types i j : I.
 
-Lemma cmE (f : {fsfun _ : I => 0%N}) : mkcmonom f =1 CMonom f.
+Lemma cmE (f : {fsfun of _ : I => 0%N}) : mkcmonom f =1 CMonom f.
 Proof. by move=> i; rewrite unlock. Qed.
 
 Lemma cmP m1 m2 : reflect (forall i, m1 i = m2 i) (m1 == m2).
@@ -1612,7 +1628,7 @@ End Structures.
 
 (* -------------------------------------------------------------------- *)
 Definition mdeg {I : choiceType} (m : {cmonom I}) :=
-  nosimpl (\sum_(k : finsupp m) (m (val k)))%N.
+  nosimpl (\sum_(k <- finsupp m) (m k))%N.
 
 Definition mnmwgt {n} (m : {cmonom 'I_n}) :=
   nosimpl (\sum_i m i * i.+1)%N.
@@ -1663,21 +1679,21 @@ apply/fsetP=> i; rewrite in_fsetU -!cmE_neq0 cmM.
 by rewrite addn_eq0 negb_and.
 Qed.
 
-Lemma mdegE m : mdeg m = (\sum_(i : finsupp m) (m (val i)))%N.
+Lemma mdegE m : mdeg m = (\sum_(i <- finsupp m) (m i))%N.
 Proof. by []. Qed.
 
 Lemma mdegEw m (d : {fset I}) : finsupp m `<=` d ->
-  mdeg m = (\sum_(i : d) (m (val i)))%N.
-Proof. 
-move=> le; pose F i := m i; rewrite mdegE (big_fset_incl F le) //.
+  mdeg m = (\sum_(i <- d) (m i))%N.
+Proof.
+move=> le; pose F i := m i; rewrite mdegE (big_fset_incl _ le) //.
 by move=> i i_in_d; rewrite -cmE_neq0 negbK => /eqP.
 Qed.
 
 Lemma mdeg1 : mdeg 1%M = 0%N.
-Proof. by rewrite mdegE mdom1 big_fset0. Qed.
+Proof. by rewrite mdegE mdom1 big_seq_fset0. Qed.
 
 Lemma mdegU k : mdeg U_(k) = 1%N.
-Proof. by rewrite mdegE mdomU big_fset1 cmUU. Qed.
+Proof. by rewrite mdegE mdomU big_seq_fset1 cmUU. Qed.
 
 Lemma mdegM : {morph mdeg: m1 m2 / (m1 * m2)%M >-> (m1 + m2)%N }.
 Proof.
@@ -1696,7 +1712,7 @@ Proof. by apply/big_morph; [apply/mdegM|apply/mdeg1]. Qed.
 Lemma mdeg_eq0I m : mdeg m = 0%N -> m = 1%M.
 Proof.
 move=> h; apply/eqP/cmP=> i; move: h; rewrite mdegE cm1.
-case: mdomP=> // ki; rewrite (bigD1 (FSetSub ki)) //= => /eqP.
+case: mdomP=> // ki; rewrite (big_fsetD1 i) //= => /eqP.
 by rewrite addn_eq0=> /andP[/eqP->].
 Qed.
 
@@ -1935,7 +1951,7 @@ Implicit Types g : {malg G[{cmonom I}]}.
 
 Local Notation mdeg := (@mdeg I).
 
-Lemma msizeE g : msize g = (\max_(m : msupp g) (mdeg (val m)).+1)%N.
+Lemma msizeE g : msize g = (\max_(m <- msupp g) (mdeg m).+1)%N.
 Proof. by apply/mmeasureE. Qed.
 
 Lemma msize_mdeg_lt g m : m \in msupp g -> (mdeg m < msize g)%N.
diff --git a/src/xfinmap.v b/src/xfinmap.v
index f6cde8e..471f546 100644
--- a/src/xfinmap.v
+++ b/src/xfinmap.v
@@ -2,7 +2,7 @@
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun.
 From mathcomp Require Import choice seq path finset finfun fintype bigop.
 From mathcomp Require Import bigenough.
-From mathcomp Require Export finmap.
+From Devel Require Export finmap.
 
 (* -------------------------------------------------------------------- *)
 Set Implicit Arguments.
@@ -17,62 +17,6 @@ Lemma fnd_fmap0 (T : choiceType) (U : Type) x :
   ([fmap] : {fmap T -> U}).[?x] = None.
 Proof. by rewrite not_fnd // in_fset0. Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma enum_fset0 (T : choiceType) :
-  enum [finType of fset0] = [::] :> seq (@fset0 T).
-Proof. by rewrite enumT unlock. Qed.
-
-Lemma enum_fset1 (T : choiceType) (x : T) :
-  enum [finType of [fset x]] = [:: [`fset11 x]].
-Proof.
-apply/perm_eq_small=> //; apply/uniq_perm_eq => //.
-  by apply/enum_uniq.
-case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=.
-by rewrite eqE /=; rewrite in_fset1 in hy.
-Qed.
-
-(* -------------------------------------------------------------------- *)
-Section BigFSet.
-Variable (R : Type) (idx : R) (op : Monoid.law idx).
-Variable (I : choiceType).
-
-Lemma big_fset0 (F : @fset0 I -> R) :
-  \big[op/idx]_(i : fset0) F i = idx.
-Proof. by rewrite /index_enum -enumT /= enum_fset0 big_nil. Qed.
-
-Lemma big_fset1 (a : I) (F : [fset a] -> R) :
-  \big[op/idx]_(i : [fset a]) F i = F (FSetSub (fset11 a)).
-Proof. by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.
-End BigFSet.
-
-Section BigFSetIncl.
-Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
-Variables (T : choiceType) (A B : {fset T}) (F : T -> R).
-
-Lemma big_fset_incl :
-    A `<=` B
-  -> (forall x, x \in B -> x \notin A -> F x = idx)
-  -> \big[op/idx]_(x : A) F (val x) = \big[op/idx]_(x : B) F (val x).
-Proof.
-move=> leAB Fid; rewrite [RHS](bigID (mem A \o val)) /=.
-rewrite [X in op _ X]big1 => [|b /Fid ->//].
-rewrite Monoid.mulm1 -[RHS]big_filter.
-rewrite -[LHS](big_map _ xpredT) -[RHS](big_map _ xpredT).
-apply/eq_big_perm/uniq_perm_eq.
-+ rewrite map_inj_uniq; last by apply/val_inj.
-  by rewrite /index_enum -enumT enum_uniq.
-+ rewrite map_inj_uniq; [apply/filter_uniq | by apply/val_inj].
-  by rewrite /index_enum -enumT enum_uniq.
-move=> x; apply/mapP/mapP=> -[] => [a _ ->|b].
-+ exists (fincl leAB a) => //; rewrite mem_filter /=.
-  by rewrite fsvalP /= /index_enum -enumT mem_enum.
-rewrite mem_filter => /andP[inA _] ->; exists [`inA] => //.
-by rewrite /index_enum -enumT mem_enum.
-Qed.
-End BigFSetIncl.
-
-Arguments big_fset_incl [R idx op T A B].
-
 (* -------------------------------------------------------------------- *)
 Module BigEnoughFSet.
 Export BigEnough.

From 23f886da8a5b82e136efe50c4554b33c752d914a Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 29 Aug 2018 09:02:36 +0200
Subject: [PATCH 2/9] Avoided finType in fsfun

---
 src/monalg.v | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/monalg.v b/src/monalg.v
index 0544ee0..e997984 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -42,8 +42,10 @@ Reserved Notation "{ 'malg' K }"
   (at level 0, K at level 2, format "{ 'malg'  K }").
 Reserved Notation "[ 'malg' g ]"
   (at level 0, g at level 2, format "[ 'malg'  g ]").
-Reserved Notation "[ 'malg' x : aT => E ]"
-  (at level 0, x ident, format "[ 'malg'  x  :  aT  =>  E ]").
+(* Reserved Notation "[ 'malg' x : aT => E ]"
+  (at level 0, x ident, format "[ 'malg'  x  :  aT  =>  E ]"). *)
+Reserved Notation "[ 'malg' x 'in' aT => E ]"
+  (at level 0, x ident, format "[ 'malg'  x  'in'  aT  =>  E ]").
 Reserved Notation "[ 'malg' x => E ]"
   (at level 0, x ident, format "[ 'malg'  x  =>  E ]").
 Reserved Notation "{ 'mpoly' T [ n ] }"
@@ -341,8 +343,8 @@ End MkMalg.
 (* -------------------------------------------------------------------- *)
 Notation "[ 'malg' g ]"
   := (mkmalg g) : ring_scope.
-Notation "[ 'malg' x : aT => E ]"
-  := (mkmalg [fsfun x : aT => E]) : ring_scope.
+Notation "[ 'malg' x 'in' aT => E ]"
+  := (mkmalg [fsfun x in aT => E]) : ring_scope.
 Notation "[ 'malg' x => E ]"
   := (mkmalg [fsfun x => E]) : ring_scope.
 Notation "<< z *g k >>"
@@ -397,7 +399,7 @@ Lemma mcoeff_fnd (g : {fmap K -> G}) k :
 Proof. by apply/fsfun_ffun. Qed.
 
 Lemma mcoeffE (domf : {fset K}) (E : K -> G) k :
-    [malg k : domf => E (val k)]@_k
+    [malg k in domf => E k]@_k
   = if k \in domf then E k else 0.
 Proof. by apply/fsfun_fun. Qed.
 
@@ -437,10 +439,10 @@ Definition fgzero : {malg G[K]} :=
   [malg x => [fmap] x].
 
 Definition fgopp g :=
-  [malg k : msupp g => - g@_(val k)].
+  [malg k in msupp g => - g@_k].
 
 Definition fgadd g1 g2 :=
-  [malg k : (msupp g1 `|` msupp g2) => g1@_(val k) + g2@_(val k)].
+  [malg k in (msupp g1 `|` msupp g2) => g1@_k + g2@_k].
 
 Lemma fgzeroE k : fgzero@_k = 0.
 Proof. by rewrite mcoeff_fnd !(in_fsetE, not_fnd). Qed.
@@ -1046,7 +1048,7 @@ Proof. by rewrite mul_malgC mcoeffZ. Qed.
 (* I don't know here how to avoid going through finType due to the use  *)
 (* of boolean [exists ...]                                              *)
 (* -------------------------------------------------------------------- *)
-Lemma msuppM_le_fintype g1 g2 k :
+Lemma msuppM_le_finType g1 g2 k :
   k \in msupp (g1 * g2) ->
         exists k1 : msupp g1, exists k2 : msupp g2, k = (val k1 * val k2)%M.
 Proof.
@@ -1063,7 +1065,7 @@ Lemma msuppM_le g1 g2 k :
   k \in msupp (g1 * g2) ->
     exists k1 k2, [/\ k1 \in msupp g1, k2 \in msupp g2 & k = (k1 * k2)%M].
 Proof.
-move/msuppM_le_fintype => [] [k1 Hk1] [] [k2 Hk2] /= Hk.
+move/msuppM_le_finType => [] [k1 Hk1] [] [k2 Hk2] /= Hk.
 by exists k1; exists k2.
 Qed.
 

From 3cd157a7db96e0bf473bb62e19cd592ca4851414 Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 29 Aug 2018 09:19:08 +0200
Subject: [PATCH 3/9] replaced [forall m : msupp g ..] by all .. (enum_fset
 (msupp g)) to get rid of val

---
 src/monalg.v | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/monalg.v b/src/monalg.v
index e997984..f912718 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -1274,7 +1274,7 @@ Context {K : choiceType} {G : zmodType}.
 
 Definition monalgOver (S : pred_class) :=
   [qualify a g : {malg G[K]} |
-     [forall m : msupp g, g@_(val m) \in S]].
+   all (fun m => g@_m \in S) (enum_fset (msupp g))].
 
 Fact monalgOver_key S : pred_key (monalgOver S). Proof. by []. Qed.
 Canonical monalgOver_keyed S := KeyedQualifier (monalgOver_key S).
@@ -1289,25 +1289,22 @@ Local Notation monalgOver := (@monalgOver K G).
 Lemma monalgOverS (S1 S2 : pred_class) :
   {subset S1 <= S2} -> {subset monalgOver S1 <= monalgOver S2}.
 Proof.
-move=> le_S1S2 g /forallP /= S1g; apply/forallP.
-by move=> /= x; apply/le_S1S2/S1g.
+move=> le_S1S2 g /allP /= S1g; apply/allP => /= x Hx.
+exact/le_S1S2/S1g.
 Qed.
 
 Lemma monalgOverU c k S :
   << c *g k >> \in monalgOver S = (c == 0) || (c \in S).
 Proof.
-rewrite qualifE msuppU; case: (c =P 0)=> [->|] /=.
-  by apply/forallP=> [[k']]; rewrite /= monalgU0 in_fset0.
-move=> nz_c; apply/forallP/idP=> /= h.
-  by move/(_ (FSetSub (fset11 k))): h; rewrite mcoeffUU.
-by case=> /= k'; rewrite in_fset1=> /eqP->; rewrite mcoeffUU.
+rewrite qualifE msuppU; case: (c =P 0)=> [->|] //=.
+move=> nz_c; apply/allP/idP=> /= [h | h x].
+  by move/(_ k): h; rewrite mcoeffUU; apply; rewrite in_fset1.
+by rewrite in_fset1=> /eqP->; rewrite mcoeffUU.
 Qed.
 
 Lemma monalgOver0 S: 0 \is a monalgOver S.
-Proof.
-rewrite qualifE msupp0; apply/forallP=> //=.
-by case=> /= x; rewrite in_fset0.
-Qed.
+Proof. by rewrite qualifE msupp0; apply/allP. Qed.
+
 End Theory.
 
 (* -------------------------------------------------------------------- *)
@@ -1323,8 +1320,8 @@ Local Notation monalgOver := (@monalgOver K G).
 Lemma monalgOverP {g} :
   reflect (forall m, g@_m \in kS) (g \in monalgOver kS).
 Proof.
-apply: (iffP forallP)=> /= h k; last by rewrite h.
-by case: msuppP=> [kg|]; rewrite ?rpred0 // (h (FSetSub kg)).
+apply: (iffP allP)=> /= h k; last by rewrite h.
+by case: msuppP=> [kg|]; rewrite ?rpred0 // (h k).
 Qed.
 
 Lemma monalgOver_addr_closed : addr_closed (monalgOver kS).
@@ -1581,7 +1578,7 @@ Definition cmu i : {cmonom I} :=
   mkcmonom [fsfun x => [fmap].[i <- 1%N] x].
 
 Definition cmmul m1 m2 : {cmonom I} := mkcmonom [fsfun
-  i : finsupp m1 `|` finsupp m2 => (m1 (val i) + m2 (val i))%N].
+  i in finsupp m1 `|` finsupp m2 => (m1 i + m2 i)%N].
 
 Lemma cmoneE i : cmone i = 0%N.
 Proof. by rewrite cmE fsfun_ffun insubF. Qed.

From eb897c0a5468ed347645a62a857280d9792e3bd4 Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 29 Aug 2018 20:54:17 +0200
Subject: [PATCH 4/9] Alternative statements to msuppM_le

---
 src/monalg.v | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/monalg.v b/src/monalg.v
index f912718..a8e34c0 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -42,8 +42,6 @@ Reserved Notation "{ 'malg' K }"
   (at level 0, K at level 2, format "{ 'malg'  K }").
 Reserved Notation "[ 'malg' g ]"
   (at level 0, g at level 2, format "[ 'malg'  g ]").
-(* Reserved Notation "[ 'malg' x : aT => E ]"
-  (at level 0, x ident, format "[ 'malg'  x  :  aT  =>  E ]"). *)
 Reserved Notation "[ 'malg' x 'in' aT => E ]"
   (at level 0, x ident, format "[ 'malg'  x  'in'  aT  =>  E ]").
 Reserved Notation "[ 'malg' x => E ]"
@@ -1045,8 +1043,6 @@ Qed.
 Lemma mcoeffCM c g k : (c%:MP * g)@_k = c * g@_k :> R.
 Proof. by rewrite mul_malgC mcoeffZ. Qed.
 
-(* I don't know here how to avoid going through finType due to the use  *)
-(* of boolean [exists ...]                                              *)
 (* -------------------------------------------------------------------- *)
 Lemma msuppM_le_finType g1 g2 k :
   k \in msupp (g1 * g2) ->
@@ -1056,11 +1052,10 @@ move=> k_in_g1Mg2; apply/(existsPP (fun _ => exists_eqP)).
 apply/contraLR: k_in_g1Mg2=> hk; rewrite -mcoeff_eq0.
 rewrite mcoeffMl big_seq big1 // => /= k1 Hk1.
 rewrite big_seq big1 // => k2 Hk2.
-case: eqP=> // kE; case/negP: hk; apply/existsP.
-by exists [` Hk1]; apply/existsP; exists [` Hk2]; rewrite kE.
+case: eqP=> // kE; case/negP: hk.
+by apply/existsP; exists [` Hk1]; apply/existsP; exists [` Hk2]; rewrite kE.
 Qed.
 
-(* -------------------------------------------------------------------- *)
 Lemma msuppM_le g1 g2 k :
   k \in msupp (g1 * g2) ->
     exists k1 k2, [/\ k1 \in msupp g1, k2 \in msupp g2 & k = (k1 * k2)%M].
@@ -1069,6 +1064,22 @@ move/msuppM_le_finType => [] [k1 Hk1] [] [k2 Hk2] /= Hk.
 by exists k1; exists k2.
 Qed.
 
+(* Alternative equivalent statement *)
+Lemma msuppM_incl g1 g2 :
+  msupp (g1 * g2) `<=` [fset (k1 * k2)%M | k1 in msupp g1, k2 in msupp g2].
+Proof.
+have sum_neq0 f (s : seq K) (H : \sum_(i <- s) f i != 0) :
+     exists2 i, i \in s & f i != 0 :> R.
+  suff : ~~ all (fun i => f i == 0) s by move/allPn => [] i Hi Hf; exists i.
+  apply/contra: H => /allP H.
+  by rewrite big_seq; apply/eqP/big1 => i /H/eqP.
+apply/fsubsetP => k.
+rewrite -mcoeff_neq0 mcoeffMl => /sum_neq0 [k1 Hk1] /sum_neq0 [k2 Hk2] H.
+apply/imfset2P; exists k1 => //; exists k2 => //.
+apply/esym/eqP; move: H; rewrite eq_sym; apply contraR => /negbTE ->.
+by rewrite mulr0n.
+Qed.
+
 (* -------------------------------------------------------------------- *)
 Lemma malgC_is_multiplicative : multiplicative (@malgC K R).
 Proof.
@@ -1478,11 +1489,11 @@ Qed.
 Lemma mmeasureN g : mmeasure (-g) = mmeasure g.
 Proof. by rewrite mmeasureE msuppN. Qed.
 
-(* Lemmas about max apply only on fintypes and not seq *)
 Lemma mmeasureD_le g1 g2 :
   (mmeasure (g1 + g2) <= maxn (mmeasure g1) (mmeasure g2))%N.
 Proof.
 rewrite {1}mmeasureE big_seq_fsetE /=.
+(* Going briefly through finType as lemmas about max apply only to them *)
 apply/bigmax_leqP=> [[i ki]] _ /=.
 have /fsubsetP /(_ i ki) := (msuppD_le g1 g2); rewrite in_fsetU.
 by rewrite leq_max; case/orP=> /mmeasure_mnm_lt->; rewrite !simpm.

From 3886c6b10fcd534784f4bd72062f2b7d6202558d Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 29 Aug 2018 21:04:40 +0200
Subject: [PATCH 5/9] Switch back to mathcomp + finset-1.1

---
 src/xfinmap.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/xfinmap.v b/src/xfinmap.v
index 471f546..3a75a87 100644
--- a/src/xfinmap.v
+++ b/src/xfinmap.v
@@ -2,7 +2,7 @@
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun.
 From mathcomp Require Import choice seq path finset finfun fintype bigop.
 From mathcomp Require Import bigenough.
-From Devel Require Export finmap.
+From mathcomp Require Export finmap.
 
 (* -------------------------------------------------------------------- *)
 Set Implicit Arguments.
@@ -12,11 +12,6 @@ Unset Printing Implicit Defensive.
 Local Open Scope fset.
 Local Open Scope fmap.
 
-(* -------------------------------------------------------------------- *)
-Lemma fnd_fmap0 (T : choiceType) (U : Type) x :
-  ([fmap] : {fmap T -> U}).[?x] = None.
-Proof. by rewrite not_fnd // in_fset0. Qed.
-
 (* -------------------------------------------------------------------- *)
 Module BigEnoughFSet.
 Export BigEnough.

From f6cec75b1564f1809199fa4321d1b9ab79355111 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 31 Aug 2018 09:32:28 +0200
Subject: [PATCH 6/9] bump opam/finmap version to 1.1.0

---
 opam | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index cfbeb7f..9eecb96 100644
--- a/opam
+++ b/opam
@@ -18,8 +18,8 @@ depends: [
   "coq" {(>= "8.5" | = "dev")}
   "coq-mathcomp-ssreflect" { (>= "1.6" | = "dev") }
   "coq-mathcomp-algebra"   { (>= "1.6" | = "dev") }
-  "coq-mathcomp-bigenough" {>= "1.0.0" & < "1.1.0~"}
-  "coq-mathcomp-finmap"    {>= "1.0.0" & < "1.1.0~"}
+  "coq-mathcomp-bigenough" {>= "1.1.0" & < "1.2.0~"}
+  "coq-mathcomp-finmap"    {>= "1.1.0" & < "1.2.0~"}
 ]
 tags: [
   "keyword:multinomials"

From 1ed69075962ff29ad89dcc09795572c9cd4893b1 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 31 Aug 2018 11:50:09 +0200
Subject: [PATCH 7/9]

---
 opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/opam b/opam
index 9eecb96..4d81b1f 100644
--- a/opam
+++ b/opam
@@ -18,7 +18,7 @@ depends: [
   "coq" {(>= "8.5" | = "dev")}
   "coq-mathcomp-ssreflect" { (>= "1.6" | = "dev") }
   "coq-mathcomp-algebra"   { (>= "1.6" | = "dev") }
-  "coq-mathcomp-bigenough" {>= "1.1.0" & < "1.2.0~"}
+  "coq-mathcomp-bigenough" {>= "1.0.0" & < "1.1.0~"}
   "coq-mathcomp-finmap"    {>= "1.1.0" & < "1.2.0~"}
 ]
 tags: [

From e0588f741e3fa74f45c63c9cfcf1118ff19704b0 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 31 Aug 2018 13:07:23 +0200
Subject: [PATCH 8/9] removing irrelevant matrix COQ="8.6.1" MATHCOMP="1.6.1"

---
 .travis.yml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index c002606..1920866 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -13,7 +13,6 @@ env:
   - COMPILER="system"
   # Main test targets
   matrix:
-  - COQ="8.6.1" MATHCOMP="1.6.1"
   - COQ="8.6.1" MATHCOMP="1.7.0"
   - COQ="8.7.2" MATHCOMP="1.7.0"
   - COQ="8.8.1" MATHCOMP="1.7.0"
@@ -21,8 +20,6 @@ env:
   - COQ="dev" MATHCOMP="1.7.0"
   - COQ="dev" MATHCOMP="dev"
 matrix:
-  allow_failures:
-  - env: COQ="8.6.1" MATHCOMP="1.6.1"
   fast_finish: true
 install:
 - sudo add-apt-repository --yes ppa:avsm/ppa

From 6efa2a3ef9a2ddd4a095b9aee2ae38268245c7f3 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 31 Aug 2018 13:07:52 +0200
Subject: [PATCH 9/9] nits

---
 src/monalg.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/monalg.v b/src/monalg.v
index a8e34c0..bb7cedb 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -1070,7 +1070,7 @@ Lemma msuppM_incl g1 g2 :
 Proof.
 have sum_neq0 f (s : seq K) (H : \sum_(i <- s) f i != 0) :
      exists2 i, i \in s & f i != 0 :> R.
-  suff : ~~ all (fun i => f i == 0) s by move/allPn => [] i Hi Hf; exists i.
+  suff: ~~ all (fun i => f i == 0) s by move/allPn => [] i Hi Hf; exists i.
   apply/contra: H => /allP H.
   by rewrite big_seq; apply/eqP/big1 => i /H/eqP.
 apply/fsubsetP => k.
@@ -1284,8 +1284,7 @@ Section Def.
 Context {K : choiceType} {G : zmodType}.
 
 Definition monalgOver (S : pred_class) :=
-  [qualify a g : {malg G[K]} |
-   all (fun m => g@_m \in S) (enum_fset (msupp g))].
+  [qualify a g : {malg G[K]} | all (fun m => g@_m \in S) (msupp g)].
 
 Fact monalgOver_key S : pred_key (monalgOver S). Proof. by []. Qed.
 Canonical monalgOver_keyed S := KeyedQualifier (monalgOver_key S).