proposition: Lemma spec_ww_add_c_cont : P x y (ww_add_c_cont x y).
proof: Proof. destruct x as [ |xh xl];trivial. apply spec_f0;trivial. destruct y as [ |yh yl]. apply spec_f0;rewrite Z.add_0_r;trivial. simpl. generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l]; intros H;unfold interp_carry in H. generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h]; intros H1;unfold interp_carry in *. apply spec_f0. simpl;rewrite H;rewrite H1;ring. apply spec_f1. simpl;rewrite spec_w_WW;rewrite H. rewrite Z.add_assoc;rewrite wwB_wBwB. rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r. rewrite Z.mul_1_l in H1;rewrite H1;ring. generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) as [h|h]; intros H1;unfold interp_carry in *. apply spec_f0;simpl;rewrite H1. rewrite Z.mul_add_distr_r. rewrite <- Z.add_assoc;rewrite H;ring. apply spec_f1. rewrite spec_w_WW;rewrite wwB_wBwB. rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r. rewrite Z.mul_1_l in H1;rewrite H1. rewrite Z.mul_add_distr_r. rewrite <- Z.add_assoc;rewrite H; simpl; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase