[WIP] replace the infrastructure of mpoly with monalg

Author: pi8027

src/monalg.v

@@ -44,7 +44,7 @@ Reserved Notation "<< k >>" (format "<< k >>").
 Reserved Notation "g @_ k"
   (at level 3, k at level 2, left associativity, format "g @_ k").
 Reserved Notation "c %:MP" (format "c %:MP").
-Reserved Notation "''X_{1..' n '}'".
+Reserved Notation "''X_{1..' n '}'" (n at level 2).
 Reserved Notation "'U_(' n )" (format "'U_(' n )").
 Reserved Notation "x ^[ f , g ]" (at level 1, format "x ^[ f , g ]").
 
@@ -1389,6 +1389,8 @@ Canonical  cmonom_unlockable k := [unlockable fun cmonom_of_fsfun k].
 
 End CmonomDef.
 
+Bind Scope monom_scope with cmonom.
+
 Notation "{ 'cmonom' I }" := (cmonom I) : type_scope.
 Notation "''X_{1..' n '}'" :=  (cmonom 'I_n) : type_scope.
 Notation "{ 'mpoly' R [ n ] }" := {malg R['X_{1..n}]} : type_scope.
@@ -1413,7 +1415,7 @@ Implicit Types (m : cmonom I).
 Lemma cmE (f : {fsfun of _ : I => 0%N}) : mkcmonom f =1 CMonom f.
 Proof. by rewrite unlock. Qed.
 
-Lemma cmP m1 m2 : reflect (forall i, m1 i = m2 i) (m1 == m2).
+Lemma cmP m1 m2 : reflect (m1 =1 m2) (m1 == m2).
 Proof. by apply: (iffP eqP) => [->//|eq]; apply/val_inj/fsfunP. Qed.
 
 Definition onecm : cmonom I := mkcmonom [fsfun of _ => 0%N].
@@ -1465,6 +1467,8 @@ HB.instance Definition _ := MonomialDef_isConomialDef.Build (cmonom I) mulcmC.
 
 End CmonomCanonicals.
 
+HB.instance Definition _ (I : countType) := [Countable of cmonom I by <:].
+
 (* -------------------------------------------------------------------- *)
 Definition mdeg {I : choiceType} (m : cmonom I) :=
   (\sum_(k <- finsupp m) m k)%N.
@@ -1659,6 +1663,8 @@ Canonical  fmonom_unlockable k := [unlockable fun fmonom_of_seq k].
 
 End FmonomDef.
 
+Bind Scope monom_scope with fmonom.
+
 Notation "{ 'fmonom' I }" := (fmonom I) : type_scope.
 
 Local Notation mkfmonom s := (fmonom_of_seq fmonom_key s).
@@ -1715,6 +1721,8 @@ HB.instance Definition _ := Choice_isMonomialDef.Build (fmonom I)
 
 End FmonomCanonicals.
 
+HB.instance Definition _ (I : countType) := [Countable of fmonom I by <:].
+
 (* -------------------------------------------------------------------- *)
 Definition fdeg (I : choiceType) (m : fmonom I) := size m.