proposition: Lemma spec_ww_add_carry_c : forall x y, [+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1.
proof: Proof. destruct x as [ |xh xl];intro y. exact (spec_ww_succ_c y). destruct y as [ |yh yl]. rewrite Z.add_0_r;exact (spec_ww_succ_c (WW xh xl)). simpl; replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring. generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_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 H1;rewrite <- H1. trivial. unfold interp_carry;repeat rewrite Z.mul_1_l;simpl;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 H1;rewrite <- H1. trivial. unfold interp_carry;rewrite spec_w_WW; repeat rewrite Z.mul_1_l;simpl;rewrite wwB_wBwB;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase