fact: Definition pow_N (x:t)(n:N) : t := match n with | BinNat.N0 => one | BinNat.Npos p => pow_pos x p end.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen