proposition: Lemma spec_ww_add_c : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
proof: Proof. destruct x as [ |xh xl];trivial. destruct y as [ |yh yl]. rewrite Z.add_0_r;trivial. 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]; intros H;unfold interp_carry in H;rewrite <- H. generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1. trivial. repeat rewrite Z.mul_1_l;rewrite spec_w_WW;rewrite wwB_wBwB; ring. rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1. simpl;ring. repeat rewrite Z.mul_1_l;rewrite wwB_wBwB;rewrite spec_w_WW;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase