proposition: Lemma coeff_prodXdiff (b : 'I_n) (k : 'X_{1..n}) : (k <= rbound b)%MM -> (\prod_(i < n | i < b) ('X_i - 'X_b))@_k = (k == mesymlm n b)%:R.
proof: Proof. Proof using. case: b => b /=. elim: {1 5 7}b (leqnn b) k => [| c IHc] Hc k Hb Hk. rewrite big1 //. suff -> : mesymlm n 0 = 0%MM by rewrite mcoeff1. by rewrite mnmP => i; rewrite !mnmE /mesymlmnm inE ltn0. set ordb := Ordinal Hb. move/(_ (ltnW Hc)) : IHc => Hrec. have Hcn := ltn_trans Hc Hb. pose ordc := Ordinal Hcn. rewrite (bigID (xpred1 ordc)) /=. rewrite (eq_bigl (xpred1 ordc)); first last. move=> i /=; case: eqP => [->|]; last by rewrite andbF. by rewrite /= ltnSn. rewrite (eq_bigl (fun i : 'I_n => i < c)); first last. by move=> i /=; rewrite ltnS ltn_neqAle [RHS]andbC. rewrite big_pred1_eq. rewrite (mcoeff_poly_mul_lin _ _ (k := (mdeg k).+2)) //. case: (boolP (U_(ordc) <= k)%MM) => Hck. - have ordc_bound : mdeg (U_(ordc))%MM < (mdeg k).+2 by rewrite mdeg1. pose mc := BMultinom ordc_bound; rewrite (bigID (xpred1 mc)) /=. rewrite (eq_bigl (xpred1 mc)); first last. move=> m /=; case eqP => [->|]; last by rewrite andbF. by rewrite /= Hck. rewrite big_pred1_eq /= coeffXdiff; last exact: lepm_trans Hck Hk. rewrite eq_refl mul1r {}Hrec; first last. apply: (lepm_trans _ Hk); apply/mnm_lepP => i. rewrite mnmBE; exact: leq_subr. rewrite big1 ?addr0; first last. move=> m /andP[Hmk Hmc1]. rewrite coeffXdiff; last exact: lepm_trans Hmk Hk. by move: Hmc1; rewrite {1}/eq_op /= => /= /negbTE /= ->; rewrite mul0r. rewrite -{2}(submK Hck). have -> : mesymlm n c.+1 = (mesymlm n c + U_(ordc))%MM. rewrite mnmP => i; rewrite !mnmE !inE ltnS leq_eqVlt. rewrite orbC eq_sym {2}/eq_op/=. case: eqP => [->|_]; first by rewrite ltnn. by rewrite orbF addn0. congr (nat_of_bool _)%:R; apply/eqP/eqP => [ <- // | Heq]. by rewrite -[RHS](addmK (U_(ordc))%MM) -[LHS](addmK (U_(ordc))%MM) Heq. - rewrite big1; first last. move=> m /= Hm; rewrite coeffXdiff; last exact: lepm_trans Hm Hk. suff -> : m == U_(ordc)%MM :> 'X_{1..n} = false by rewrite mul0r. apply/negP => /eqP; rewrite mnmP => /(_ ordc). rewrite mnm1E eq_refl /= => Habs; move: Hck. have : (U_(ordc) <= m)%MM by rewrite lep1mP {}Habs. by move/lepm_trans/(_ Hm) => ->. suff -> : (k == mesymlm n c.+1) = false by []. apply/negP => /eqP; rewrite mnmP => /(_ ordc). move: Hck; rewrite lep1mP negbK => /eqP ->. by rewrite /mesymlm /mesymlmnm /mesym1 /= mnmE inE /= ltnSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition