proposition: Lemma spec_ww_succ : forall x, [[ww_succ x]] = ([[x]] + 1) mod wwB.
proof: Proof. destruct x as [ |xh xl];simpl. rewrite spec_ww_1;rewrite Zmod_small;trivial. split;[intro;discriminate|apply wwB_pos]. rewrite <- Z.add_assoc;generalize (spec_w_succ_c xl); destruct (w_succ_c xl) as[l|l];intro H;unfold interp_carry in H;rewrite <-H. rewrite Zmod_small;trivial. rewrite wwB_wBwB;apply beta_mult;apply spec_to_Z. assert ([|l|] = 0). clear spec_ww_1 spec_w_1 spec_w_0. assert (H1:= spec_to_Z l); assert (H2:= spec_to_Z xl); lia. rewrite H0;rewrite Z.add_0_r;rewrite <- Z.mul_add_distr_r;rewrite wwB_wBwB. rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite spec_w_W0;rewrite spec_w_succ;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase