proposition: Lemma spec_ww_karatsuba_c : forall x y, [||ww_karatsuba_c x y||]=[[x]]*[[y]].
proof: Proof. intros x y; unfold ww_karatsuba_c;apply spec_double_mul_c. intros; apply spec_kara_prod; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase