proposition: Lemma spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB.
proof: Proof. Proof using w_0 spec_ww_Bm1 spec_w_WW spec_w_Bm1 spec_to_Z spec_pred_c spec_pred. destruct x as [ |xh xl];simpl. apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial. rewrite spec_ww_Bm1;ring. replace ([|xh|]*wB + [|xl|] - 1) with ([|xh|]*wB + ([|xl|] - 1)). 2:ring. generalize (spec_pred_c xl);destruct (w_pred_c xl) as [l|l];intro H; unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. rewrite Zmod_small. apply spec_w_WW. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh l)). rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. change ([|xh|] + -1) with ([|xh|] - 1). assert ([|l|] = wB - 1). assert (H1:= spec_to_Z l);assert (H2:= spec_to_Z xl); lia. rewrite (mod_wwB w_digits w_to_Z);trivial. rewrite spec_pred;rewrite spec_w_Bm1;rewrite <- H0;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase