proposition: Theorem b2n_spec: [|b2n|] = 2 ^ [|n|] * [|b|].
proof: Proof. unfold b2n, w_add_mul_div; case n_spec; intros Hp Hp1. assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto with zarith. intros H1; contradict Hp1; apply Zle_not_lt; unfold base. apply Z.le_trans with (2 ^ [|n|] * 1); auto with zarith. rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. rewrite ZnZ.spec_add_mul_div; auto with zarith. rewrite _w0_is_0; rewrite Zdiv_0_l; auto with zarith. rewrite Zplus_0_r; rewrite Zmult_comm; apply Zmod_small; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux