proposition: Lemma log2_digits_head0 : forall x, 0 < [x] -> [log2 x] = Zpos (digits x) - [head0 x] - 1.
proof: Proof. intros. rewrite log2_fold. rewrite spec_eqb. rewrite spec_0. case Z.eqb_spec. auto with zarith. intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x). rewrite ZnZ.spec_sub_carry. intros. generalize (head0_zdigits n x H). generalize (ZnZ.spec_to_Z (ZnZ.head0 x)). generalize (ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). rewrite ZnZ.spec_zdigits. intros. apply Zmod_small. auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen