fact: Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := match i with | xH => x | xO i => let p := pow_pos x i in p * p | xI i => let p := pow_pos x i in x * (p * p) end.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax