proposition: Lemma wB_pos: 1 < wB.
proof: Proof. unfold base;apply Z.lt_le_trans with (2^1). unfold Z.lt;reflexivity. apply Zpower_le_monotone. unfold Z.lt;reflexivity. split;unfold Z.le;intros H. discriminate H. clear spec_w_0W w_0W spec_w_Bm1 spec_to_Z spec_w_WW w_WW. destruct w_digits; discriminate H. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType