proposition: Lemma mpolyOverS (S1 S2 : {pred R}) : {subset S1 <= S2} -> {subset mpolyOver S1 <= mpolyOver S2}.
proof: Proof. move=> sS12 p /(all_nthP 0)S1p. by apply/(all_nthP 0)=> i /S1p; apply: sS12. 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