proposition: Lemma spec_ww_mul_c : forall x y, [||ww_mul_c x y||] = [[x]] * [[y]].
proof: Proof. intros x y;unfold ww_mul_c;apply spec_double_mul_c. intros xh xl yh yl hh ll H1 H2. generalize (spec_ww_add_c (w_mul_c xh yl) (w_mul_c xl yh)); destruct (ww_add_c (w_mul_c xh yl) (w_mul_c xl yh)) as [c|c]; unfold interp_carry;repeat rewrite spec_w_mul_c;intros H; (rewrite spec_w_0 || rewrite spec_w_1);rewrite H;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase