proposition: Lemma spec_ww_add_mul_div : forall x y p, [|p|] <= Zpos _ww_digits -> [| add_mul_div p x y |] = ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos _ww_digits) - [|p|]))) mod wwB.
proof: Proof. refine (@spec_ww_add_mul_div t w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_digits w_zdigits low w_to_Z _ _ _ _ _ _ _ _ _ _ _);wwauto. exact ZnZ.spec_zdigits. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleAdd DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv CyclicAxioms