proposition: Lemma spec_aux_shift n p : spec_hpoly_aux n p = spec_hpoly_aux 0%N p * 'X^n.
proof: Proof. have shift_polyC (c : C) m : match m with | O => if (c == 0)%C then 0 else if (c == 1)%C then 1 else (spec c)%:P | S O => if (c == 0)%C then 0 else if (c == 1)%C then 'X : {poly R} else (spec c) *: 'X | S m => if (c == 0)%C then 0 else if (c == 1)%C then 'X^(S m) else (spec c) *: 'X^(S m) end = (if (c == 0)%C then 0 else if (c == 1)%C then 1 else (spec c)%:P) * 'X^m. case: m=> [|m] /=; first by rewrite expr0 mulr1. by case: m=> [|m] /=; rewrite ?expr1 -mul_polyC; case: ifP=> _; rewrite ?mul0r //; case: ifP=> _; rewrite ?mul1r. elim: p n=> [c n|c m p ih n] //=. case: ifP=> _ //. have -> : (if (n == 0)%N then (spec (cast m : N) : nat) else (spec (cast m : N) + n)%N) = (spec (cast m : N) + n)%N. by case: n=> [|n] /=; rewrite ?addn0. rewrite shift_polyC ih [in RHS]ih. by case: ifP=> c0; rewrite ?mulrDl -mulrA -exprD // c0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)