proposition: Lemma spec_mul_add: forall x y z, let (zh, zl) := mul_add x y z in [||WW zh zl||] = [|x|] * [|y|] + [|z|].
proof: Proof. intros x y z. refine (spec_w_mul_add _ _ _ _ _ _ _ _ _ _ _ _ x y z); auto. exact ZnZ.spec_0. exact ZnZ.spec_to_Z. exact ZnZ.spec_succ. exact ZnZ.spec_add_c. exact ZnZ.spec_mul_c. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleAdd DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv CyclicAxioms