proposition: Lemma alternate_MX (p : {poly R}) k: alternate ('X ^+ k * p) -> alternate p.
proof: Proof. elim: k => [ | k IH]; first by rewrite expr0 mul1r. case h : (p == 0); first by rewrite (eqP h) mulr0. rewrite mulrC polyseqMXn //=; last by rewrite h. by rewrite ltxx eqxx -polyseqMXn ?h // mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol