fact: Fixpoint spec_hpoly_aux n (p : @hpoly pos C) : {poly R} := match p with | Pc c => match n 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 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 | PX a m p => let mon := match n with | O => if (a == 0)%C then 0 else if (a == 1)%C then 1 else (spec a)%:P | S O => if (a == 0)%C then 0 else if (a == 1)%C then 'X else (spec a) *: 'X | S k => if (a == 0)%C then 0 else if (a == 1)%C then 'X^(S k) else (spec a) *: 'X^(S k) end in if (eq0_hpoly p) then mon else let k := if (n == 0)%N then (spec (cast m : N) : nat) else (spec (cast m : N) + n)%N in if (a == 0)%C then (spec_hpoly_aux k p) else (spec_hpoly_aux k p) + mon end.
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)