proposition: Lemma dhomog_nemf_coeff d p m: p \is d.-homog -> mf m != d -> p@_m = 0.
proof: Proof. move/dhomogP=> hg_p; apply/contraTeq; rewrite -mcoeff_msupp. by move/hg_p=> ->; rewrite negbK. 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