fact: Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := match P with | Pc c => [c] | PX P i n Q => let x := nth 0 i l in let xn := pow_pos x n in (Pphi l P) * xn + (Pphi l Q) end.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring