fact: Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R := match i with | xH => x | xO i => let p := pow_pos_gen m x i in m p p | xI i => let p := pow_pos_gen m x i in m x (m p p) end.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring