fact: Definition pow_pos x p := match x with | Pos nx => Pos (NN.pow_pos nx p) | Neg nx => match p with | xH => x | xO _ => Pos (NN.pow_pos nx p) | xI _ => Neg (NN.pow_pos nx p) end end.
imports: ZArith Lia BigNumPrelude NSig ZSig