proposition: Lemma variation_pmull a b c : c > 0 -> variation (a * c) (b) = variation a b.
proof: Proof. by move=> c_gt0; rewrite /variation mulrAC pmulr_llt0. 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)