proposition: Lemma spec_ww_opp_carry : forall x, [[ww_opp_carry x]] = wwB - [[x]] - 1.
proof: Proof. destruct x as [ |xh xl];simpl. rewrite spec_ww_Bm1;ring. rewrite spec_w_WW;simpl;repeat rewrite spec_opp_carry;rewrite wwB_wBwB;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase