proposition: Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
proof: Proof. destruct x as [ |xh xl];intros y. rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct y as [ |yh yl]. change [[W0]] with 0;rewrite Z.add_0_r. rewrite Zmod_small;trivial. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)). simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring. generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l]; unfold interp_carry;intros H;simpl;rewrite <- H. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add;trivial. rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase