proposition: Lemma spec_log2_pos : forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1).
proof: Proof. intros x H. rewrite log2_fold. rewrite spec_eqb. rewrite spec_0. case Z.eqb_spec. auto with zarith. clear H. destr_t x as (n,x). intros H. rewrite ZnZ.spec_sub_carry. assert (H0 := ZnZ.spec_to_Z x). assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). assert (H3 := head0_zdigits n x). rewrite Zmod_small by auto with zarith. rewrite Z.sub_simpl_r. rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. rewrite <- 2 Zpower_exp; auto with zarith. rewrite !Z.add_sub_assoc, !Z.add_simpl_l. rewrite ZnZ.spec_zdigits. rewrite pow2_pos_minus_1 by (red; auto). apply ZnZ.spec_head0; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen