proposition: Lemma cross_pmul p q a b : q.[a] > 0 -> q.[b] > 0 -> cross (p * q) a b = cross p a b.
proof: Proof. by move=> qa0 qb0; rewrite /cross !hornerM variation_pmull ?variation_pmulr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)