proposition: Lemma wB_div_plus : forall x y p, 0 <= p -> ([|x|]*wB + [|y|]) / 2^(Zpos w_digits + p) = [|x|] / 2^p.
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros x y p Hp;rewrite Zpower_exp;auto with zarith. rewrite <- Zdiv_Zdiv;auto with zarith. rewrite wB_div;trivial. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType