proposition: Lemma homog_prod (s : seq {mpoly R[n]}) : all (fun p => p \is homog) s -> \prod_(p <- s) p \is homog.
proof: Proof. move=> homs; apply/homogP; elim: s homs => [_ | p s ihs] /=. by exists 0%N; rewrite big_nil; apply/dhomog1. case/andP=> /homogP [dp p_hdp] {}/ihs [d ih]. by exists (dp + d)%N; rewrite big_cons; apply/dhomogM. 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