proposition: Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.
proof: Proof. intros x H. rewrite log2_fold. rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen