fact: Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := match p with | xH => subst_l (Pmul P res) | xO p => Ppow_pos (Ppow_pos res P p) P p | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p)) end.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring