fact: Variable spec_w_add_mul_div : forall x y p, [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + [|y|] / (Z.pow 2 ((Zpos w_digits) - [|p|]))) mod wB.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase