proposition: Lemma spec_add_mul_divp : forall x y, [| w_add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.
proof: Proof. intros;apply spec_add_mul_div;auto. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase