fact: Fixpoint power_pos (x:t) (p:positive) {struct p} : t := match p with | xH => x | xO p => square (power_pos x p) | xI p => mul (square (power_pos x p)) x end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1