proposition: Lemma spec_ww_succ_c : forall x, [+[ww_succ_c x]] = [[x]] + 1.
proof: Proof. Proof using w_1 spec_ww_1 spec_w_succ_c spec_w_0 spec_to_Z. destruct x as [ |xh xl];simpl. apply spec_ww_1. generalize (spec_w_succ_c xl);destruct (w_succ_c xl) as [l|l]; intro H;unfold interp_carry in H. simpl;rewrite H;ring. rewrite <- Z.add_assoc;rewrite <- H;rewrite Z.mul_1_l. assert ([|l|] = 0). generalize (spec_to_Z xl)(spec_to_Z l); lia. rewrite H0;generalize (spec_w_succ_c xh);destruct (w_succ_c xh) as [h|h]; intro H1;unfold interp_carry in H1. simpl;rewrite H1;rewrite spec_w_0;ring. unfold interp_carry;simpl ww_to_Z;rewrite wwB_wBwB. assert ([|xh|] = wB - 1). generalize (spec_to_Z xh)(spec_to_Z h); lia. rewrite H2;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase