proposition: Theorem mult_wwB: forall x y, [|x|] * [|y|] < wwB.
proof: Proof. intros x y; rewrite wwB_wBwB; rewrite Z.pow_2_r. generalize (spec_to_Z x); intros U. generalize (spec_to_Z y); intros U1. nia. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase