proposition: Lemma log2_fold : log2 = fun x => if eqb x zero then zero else iter_t log2n x.
proof: Proof. red_t; reflexivity. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen