proposition: Lemma spec_ww_pred_c : forall x, [-[ww_pred_c x]] = [[x]] - 1.
proof: Proof. Proof using w_0 spec_ww_Bm1 spec_w_WW spec_w_Bm1 spec_to_Z spec_pred_c. destruct x as [ |xh xl];unfold ww_pred_c. unfold interp_carry;rewrite spec_ww_Bm1;simpl ww_to_Z;ring. simpl ww_to_Z;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]; intros H;unfold interp_carry in H;rewrite <- H. simpl;apply spec_w_WW. rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. assert ([|l|] = wB - 1). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);lia. rewrite H0;change ([|xh|] + -1) with ([|xh|] - 1). generalize (spec_pred_c xh);destruct (w_pred_c xh) as [h|h]; intros H1;unfold interp_carry in H1;rewrite <- H1. simpl;rewrite spec_w_Bm1;ring. assert ([|h|] = wB - 1). assert (H3:= spec_to_Z h);assert (H2 := spec_to_Z xh); lia. rewrite H2;unfold interp_carry;rewrite spec_ww_Bm1;rewrite wwB_wBwB;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase