proposition: Lemma msym_fundamental_un0 (t : {mpoly R[n]}) : t \mPo S = 0 -> t = 0.
proof: Proof. set S := S; move/eqP; apply/contraTeq=> nz_t; rewrite -mleadc_eq0. have h m: m \in msupp t -> mlead (t@_m *: (XS m)) = mlead (XS m). move=> m_in_t; rewrite mleadZ_proper // mleadc_XS. by rewrite mulr1 mcoeff_eq0 m_in_t. rewrite comp_mpolyEX mlead_sum ?filter_predT; last first. rewrite (iffLR (eq_in_map _ _ _) h) -/S. apply/(@uniqP _ 0%MM) => i j; rewrite size_map. move=> lti ltj; rewrite !(nth_map 0%MM) // => /free_XS. exact: (can_in_inj (nthK _ _)). rewrite big_seq (eq_bigr _ h) -big_seq. case: (eq_bigjoin (fun m => mlead (XS m)) _ (r := msupp t)). exact/le_total. by rewrite msupp_eq0. move=> /= m m_in_t /eqP/esym; rewrite -/S=> lmm. rewrite -lmm raddf_sum /= (bigD1_seq m) //= mcoeffZ. rewrite mleadc_XS mulr1 big_seq_cond big1. by rewrite addr0 mcoeff_eq0 m_in_t. move=> /= m' /andP[m'_in_t ne_m'm]; rewrite mcoeffZ. rewrite [X in _*X]mcoeff_gt_mlead ?mulr0 //. rewrite lt_neqAle (contra_neq (@free_XS _ _)) //= lmm. exact: (joins_sup_seq (fun m => mlead (XS m))). 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