proposition: Lemma dhomog_submod_closed d : submod_closed [in R[n], d.-homog].
proof: Proof. split=> [|c p q]; first by rewrite dhomogE msupp0. move=> /dhomogP hg_p /dhomogP hg_q; apply/dhomogP=> m. move/msuppD_le; rewrite mem_cat; case/orP=> [/msuppZ_le|]. by move/hg_p. by move/hg_q. 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