proposition: Lemma mulXnC (p : {poly R}) n : p * 'X^n = 'X^n * p.
proof: Proof. apply/polyP=> i. by rewrite coefMXn coefXnM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)