proposition: Lemma lt_wB_wwB : wB < wwB.
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. unfold base;apply Zpower_lt_monotone;auto with zarith. assert (0 < Zpos w_digits). compute;reflexivity. unfold ww_digits;rewrite Pos2Z.inj_xO;auto with zarith. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType