proposition: Lemma monom_rcons (a : R) (x : seq R) i e : size x = size e -> monomial (rcons x a) (rcons e i) = (monomial x e) * a ^ i.
proof: Proof. by move => Hxe; rewrite /monomial !zip_rcons // big_rcons. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp