proposition: Lemma spec_ww_opp_c : forall x, [-[ww_opp_c x]] = -[[x]].
proof: Proof. Proof using ww_Bm1 w_Bm1 spec_w_0 spec_to_Z spec_opp_carry spec_opp_c. destruct x as [ |xh xl];simpl. reflexivity. rewrite Z.opp_add_distr;generalize (spec_opp_c xl);destruct (w_opp_c xl) as [l|l];intros H;unfold interp_carry in H;rewrite <- H; rewrite <- Z.mul_opp_l. assert ([|l|] = 0). assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);lia. rewrite H0;generalize (spec_opp_c xh);destruct (w_opp_c xh) as [h|h];intros H1;unfold interp_carry in *;rewrite <- H1. assert ([|h|] = 0). assert (H3:= spec_to_Z h);assert (H2 := spec_to_Z xh);lia. rewrite H2;reflexivity. simpl ww_to_Z;rewrite wwB_wBwB;rewrite spec_w_0;ring. unfold interp_carry;simpl ww_to_Z;rewrite wwB_wBwB;rewrite spec_opp_carry; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase