fact: Definition power_pos (x : t) p : t := match x with | Qz zx => Qz (ZZ.pow_pos zx p) | Qq nx dx => Qq (ZZ.pow_pos nx p) (NN.pow_pos dx p) end.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig