fact: Fixpoint pow_pos (x:t)(p:positive) : t := match p with | xH => x | xO p => square (pow_pos x p) | xI p => mul (square (pow_pos x p)) x end.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen