fact: Definition log2 : t -> t := Eval red_t in let log2 := iter_t log2n in fun x => if eqb x zero then zero else log2 x.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen