Merge pull request #105 from proux01/minor-cleanup

Doc typos and minor cleanup

Author: pi8027

src/mpoly.v

@@ -16,18 +16,18 @@
 (*                       delimited by %MM                                     *)
 (* [multinom E i | i < n]                                                     *)
 (*                    == the monomial in n variables whose i-th power is E(i) *)
-(*             mdeg m == the degree of the monomial m; i.e.                   *)
-(*                         mdeg m = \sum_(i < n) (m i)                        *)
+(*             mdeg m == the degree of the monomial m;                        *)
+(*                       i.e. mdeg m = \sum_(i < n) (m i)                     *)
 (*      'X_{1..n < k} == the finite type of monomials in n variables with     *)
 (*                       degree bounded by k.                                 *)
-(*      (m1 <= m2)%MM == the point-wise partial order over monomials, i.e.    *)
-(*                         (m1 <= m2)%MM <=> forall i, m1 i <= m2 i           *)
+(*      (m1 <= m2)%MM == the point-wise partial order over monomials,         *)
+(*                       i.e. (m1 <= m2)%MM <=> forall i, m1 i <= m2 i        *)
 (*       (m1 <= m2)%O == the total cpo (equipped with a cpoType) over         *)
 (*                       monomials. This is the degrevlex monomial ordering.  *)
 (* 0, 'U_i, m1 + m2,  == 'X_{1..n} is equipped with a semi-group structure,   *)
 (* m1 - m2, m *+ n, ...  all operations being point-wise. The substraction    *)
-(*                       is truncated when (m1 <= m2)%MM does not hold.       *)
-(*      mlcm m1 m2    == the monomial that is the least common multiple       *)
+(*                       is truncated when (m2 <= m1)%MM does not hold.       *)
+(*         mlcm m1 m2 == the monomial that is the least common multiple       *)
 (*       {mpoly R[n]} == the type of multivariate polynomials in n variables  *)
 (*                       and with coefficients of type R represented as       *)
 (*                       {free 'X_{1..n} / R}, i.e. as a formal sum over      *)
@@ -52,16 +52,16 @@
 (*                       monomial of p for the degrevlex monimial ordering.   *)
 (*                       mlead p defaults to 0%MM when p is 0.                *)
 (*            mlast p == the smallest non-zero monomial of p for the          *)
-(*                         degrevlex monimial ordering.                       *)
+(*                       degrevlex monimial ordering.                         *)
 (*                       mlast p defaults to 0%MM when p is 0.                *)
 (*           mleadc p == the coefficient of the highest monomial in p;        *)
 (*                       this is a notation for p@_(mlead p).                 *)
 (* p \is a mpolyOver S <=> the coefficients of p satisfy S; S should have a   *)
 (*                       key that should be (at least) an addrPred.           *)
 (*             p.@[x] == the evaluation of a polynomial p at a point x, where *)
-(*                       v is a n.-tuple R s.t. 'X_i evaluates to (tnth v i)  *)
-(*             p^`M() == formal derivative of p w.r.t the i-th variable       *)
-(*         p^`M(n, i) == formal n-derivative of p w.r.t the i-th variable     *)
+(*                       x is a n.-tuple R s.t. 'X_i evaluates to (tnth x i)  *)
+(*            p^`M(i) == formal derivative of p w.r.t the i-th variable       *)
+(*         p^`M(i, n) == formal n-derivative of p w.r.t the i-th variable     *)
 (*            p^`M[m] == formal parallel (m i)-derivative of p w.r.t the      *)
 (*                       i-th variable, i ranging in {0..n.-1}.               *)
 (*          p \mPo lq == multivariate polynomial composition, where lq is a   *)
@@ -4133,9 +4133,7 @@ apply/eqP; rewrite eq_sym eqEcard; apply/andP; split.
   apply/negP=> /imsetP [/=] x _ /eqP.
   by rewrite eqE /= eq_sym ltn_eqF.
 have := disjoint_S n k; rewrite -leq_card_setU=> /eqP->.
-rewrite !card_imset //= ?card_draws /=;
-  try exact/inj_swiden; try exact/inj_mDswiden.
-  (* remove the line above once requiring Coq >= 8.17 *)
+rewrite !card_imset //= ?card_draws /=.
 by rewrite !card_ord binS.
 Qed.