proposition: Lemma rpred_mhorner : {in mpolyOver S, forall p (v : 'I_n -> R), [forall i : 'I_n, v i \in S] -> p.@[v] \in S}.
proof: Proof. move=> p /mpolyOverP Sp v Sv; rewrite mevalE rpred_sum // => m _. rewrite rpredM // rpred_prod //= => /= i _. by rewrite rpredX //; move/forallP: Sv; apply; apply/mem_tnth. 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