proposition: Lemma double_wB_more_digits: forall n, wB <= double_wB n.
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros n; elim n; clear n; auto. unfold double_wB, "<<"; auto with zarith. intros n H1; rewrite <- double_wB_wwB. apply Z.le_trans with (wB * 1). rewrite Z.mul_1_r; apply Z.le_refl. unfold base; auto with zarith. apply Z.mul_le_mono_nonneg; auto with zarith. apply Z.le_trans with wB; auto with zarith. unfold base. rewrite <- (Z.pow_0_r 2). apply Z.pow_le_mono_r; auto with zarith. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType