proposition: Lemma msupp_rem (p : {mpoly R[n]}) m : perm_eq (msupp (p - p@_m *: 'X_[m])) (rem m (msupp p)).
proof: Proof. case: (boolP (m \in msupp p)) => h. apply/uniq_perm; rewrite ?rem_uniq //. move=> m'; rewrite mem_rem_uniq // inE /=. rewrite !mcoeff_msupp mcoeffB mcoeffZ mcoeffX. case: (eqVneq m' m) => [->|] /=. by rewrite mulr1 subrr eqxx. by rewrite mulr0 subr0. have/rem_id -> := h; move: h. rewrite mcoeff_msupp negbK=> /eqP ->. by rewrite scale0r subr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg