proposition: Lemma mcoeff_arbound b : b < n -> (abound b)@_(rbound b) = 1.
proof: Proof. Proof using. elim: b => [Hb | b IHb Hb1]. rewrite /abound {Hb} big1; first last. by move=> [i j] /= /andP[/leq_trans /[apply]]. rewrite mcoeff1 /=. suff -> : rbound 0 = 0%MM by rewrite eq_refl. by rewrite mnmP => i; rewrite mnmE. move/(_ (ltnW Hb1)): IHb => Hrec. rewrite /abound (bigID (fun p : 'II_n => p.2 <= b)) /=. rewrite (eq_bigl (fun p : 'II_n => p.1 < p.2 <= b)); first last. move=> [i j]/=; case: (leqP j b); last by rewrite !andbF. by rewrite -ltnS => /ltnW ->; rewrite !andbT. rewrite mulrC -/(abound _). pose ordb1 := Ordinal Hb1. rewrite [X in X * _](_ : _ = \prod_(i : 'I_n | i <= b) ('X_i - 'X_ordb1)); first last. rewrite (eq_bigl (fun p : 'II_n => (p.1 <= b) && (p.2 == ordb1))); first last. move=> [i j]/=; rewrite -ltnNge -andbA -eqn_leq. case: eqP => Hj. - have -> : j = ordb1 by apply val_inj. by rewrite eq_refl /= ltnS. - suff -> : (j == ordb1) = false by rewrite !andbF. by apply negbTE; move: Hj => /eqP; apply contra => /eqP ->. rewrite (reindex (fun i : 'I_n => (i, ordb1))) /=; first last. exists (fun p : 'II_n => p.1) => //. by move=> [i j] /=; rewrite inE /= => /andP[_ /eqP<-]. by apply eq_bigl => i; rewrite eq_refl andbT. rewrite (mcoeff_poly_mul_lin _ _ (k := (mdeg (rbound b.+1)).+1)) //. have /= := @coeff_prodXdiff ordb1. rewrite (eq_bigl (fun i : 'I_(_) => i <= b)); last by move=> i; rewrite ltnS. move=> Hprod. have Hmesymlm : mdeg (mesymlm n b.+1) < (mdeg (rbound b.+1)).+1. rewrite ltnS /mdeg !big_tuple; apply leq_sum => i _. by rewrite -!mnm_tnth; move: (mesymlm_rbound b.+1) => /mnm_lepP; apply. pose msmb := BMultinom Hmesymlm. rewrite (bigID (xpred1 msmb)) /=. rewrite (eq_bigl (xpred1 msmb)); first last. move=> m /=; case: eqP => [->|]; last by rewrite andbF. by rewrite /= mesymlm_rbound. rewrite big_pred1_eq /= {}Hprod ?mesymlm_rbound // eq_refl mul1r. rewrite big1 ?addr0; first last. move=> m /andP[Hm Hneq]. rewrite (eq_bigl (fun i : 'I_(_) => i < b.+1)); first last. by move=> i; rewrite ltnS. rewrite (@coeff_prodXdiff ordb1) //. by move: Hneq; rewrite {1}/eq_op/= => /negbTE -> /=; rewrite mul0r. rewrite -Hrec; congr mcoeff. rewrite mnmP => i; rewrite !mnmE inE ltnS. case: leqP => /= Hi. - by rewrite subnAC subSS subn0. - by rewrite subn0; move: Hi (ltnW Hi); rewrite /leq => /eqP -> /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition