proposition: Lemma spec_aux_shift n s : spec_seqpoly_aux n s = spec_seqpoly_aux 0 s * 'X^n.
proof: Proof. elim: s n=> [n|a s ih n] /=; first by rewrite mul0r. simpC; case: ifP=> _. by rewrite ih [in RHS]ih exprS expr1 mulrA. have h : (if n == 0%N then if (a ==1)%C then 1 else (spec a)%:P else if (a == 1)%C then if n == 1%N then 'X : {poly R} else 'X^n else spec a *: (if n == 1%N then 'X else 'X^n)) = (if (a == 1)%C then 1 else (spec a)%:P) * 'X^n. case: n=> [|n] /=; simpC. rewrite expr0 mulr1. by case: ifP=> [/eqP a1|_]. case: ifP=> [/eqP a1|_]. rewrite mul1r. by case: ifP; move/eqP=> // ->; rewrite expr1. rewrite mul_polyC. by case: ifP; move/eqP=> // ->; rewrite expr1. case: ifP=> _; first by rewrite h. rewrite ih [in RHS]ih mulrDl exprS expr1 mulrA. exact: congr2. 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)