proposition: Lemma spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
proof: Proof. destruct y as [ |yh yl];simpl. ring_simplify ([[x]] - 0);rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. destruct x as [ |xh xl];simpl. exact (spec_ww_opp (WW yh yl)). replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|])) with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|])). 2:ring. generalize (spec_sub_c xl yl);destruct (w_sub_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. simpl ww_to_Z;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