proposition: Lemma spec_ww_opp : forall x, [[ww_opp x]] = (-[[x]]) mod wwB.
proof: Proof. Proof using ww_Bm1 w_Bm1 spec_w_0 spec_to_Z spec_opp_carry spec_opp_c spec_opp. destruct x as [ |xh xl];simpl. reflexivity. rewrite Z.opp_add_distr, <- Z.mul_opp_l. generalize (spec_opp_c xl);destruct (w_opp_c xl) as [l|l];intros H;unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. rewrite spec_w_0;rewrite Z.add_0_r;rewrite wwB_wBwB. assert ([|l|] = 0). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl); lia. rewrite H0;rewrite Z.add_0_r; rewrite Z.pow_2_r; rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite spec_opp;trivial. apply Zmod_unique with (q:= -1). exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW (w_opp_carry xh) l)). rewrite spec_opp_carry;rewrite wwB_wBwB;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase