proposition: Lemma to_Z_div_minus_p : forall x p, 0 < [|p|] < Zpos w_digits -> 0 <= [|x|] / 2 ^ (Zpos w_digits - [|p|]) < 2 ^ [|p|].
proof: Proof. intros x p H;Spec_w_to_Z x. split. apply Zdiv_le_lower_bound;zarith. apply Zdiv_lt_upper_bound. zarith. rewrite <- Zpower_exp by zarith. ring_simplify ([|p|] + (Zpos w_digits - [|p|])); unfold base in HH;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub