proposition: Lemma spec_ww_mul : forall x y, [[ww_mul x y]] = [[x]]*[[y]] mod wwB.
proof: Proof. assert (U:= lt_0_wB w_digits). assert (U1:= lt_0_wwB w_digits). intros x y; case x; auto; intros xh xl. case y; auto. simpl; rewrite Z.mul_0_r; rewrite Zmod_small; auto with zarith. intros yh yl;simpl. repeat (rewrite spec_ww_add || rewrite spec_w_W0 || rewrite spec_w_mul_c || rewrite spec_w_add || rewrite spec_w_mul). rewrite <- Zplus_mod; auto with zarith. repeat (rewrite Z.mul_add_distr_r || rewrite Z.mul_add_distr_l). rewrite <- Zmult_mod_distr_r; auto with zarith. rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB; auto with zarith. rewrite Zplus_mod; auto with zarith. rewrite Zmod_mod; auto with zarith. rewrite <- Zplus_mod; auto with zarith. match goal with |- ?X mod _ = _ => rewrite <- Z_mod_plus with (a := X) (b := [|xh|] * [|yh|]) end; auto with zarith. f_equal; auto; rewrite wwB_wBwB; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase