proposition: Lemma dhomog_prod {l} (dt : l.-tuple nat) (mt : l.-tuple {mpoly R[n]}) : (forall i : 'I_l, tnth mt i \is (tnth dt i).-homog) -> \prod_(i <- mt) i \is (\sum_(i <- dt) i).-homog.
proof: Proof. elim: l dt mt => [| l ihl] dt mt hom. by rewrite tuple0 big_nil tuple0 big_nil dhomog1. case/tupleP: dt hom => d dt; case/tupleP: mt => p mt /= hom. rewrite !big_cons; apply/dhomogM. by move: (hom ord0); rewrite (tnth_nth 0) (tnth_nth 0%N). apply/ihl => i; have:= hom (inord i.+1). by rewrite !(tnth_nth 0) ?(tnth_nth 0%N) !inordK ?ltnS. 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