proposition: Lemma wB_div : forall x y, ([|x|] * wB + [|y|]) / wB = [|x|].
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros x y;unfold base;rewrite Zdiv_shift_r;auto with zarith. rewrite Z_div_mult;auto with zarith. destruct (spec_to_Z x);trivial. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType