proposition: Lemma spec_ww_sub_carry : forall x y, [[ww_sub_carry x y]] = ([[x]] - [[y]] - 1) mod wwB.
proof: Proof. destruct y as [ |yh yl];simpl. ring_simplify ([[x]] - 0);exact (spec_ww_pred x). destruct x as [ |xh xl];simpl. apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial. fold (ww_opp_carry (WW yh yl)). rewrite (spec_ww_opp_carry (WW yh yl));simpl ww_to_Z;ring. replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|]) - 1) with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|] - 1)). 2:ring. generalize (spec_sub_carry_c xl yl);destruct (w_sub_carry_c xl yl)as[l|l]; intros H;unfold interp_carry in H;rewrite <- H;rewrite spec_w_WW. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub;trivial. rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase