proposition: Lemma spec_ww_to_Z : forall x, 0 <= [[x]] < wwB.
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. destruct x as [ |h l];simpl. split;[apply Z.le_refl|apply lt_0_wwB]. assert (H:=spec_to_Z h);assert (L:=spec_to_Z l);split. apply Z.add_nonneg_nonneg;auto with zarith. rewrite <- (Z.add_0_r wwB);rewrite wwB_wBwB; rewrite Z.pow_2_r; apply beta_lex_inv;auto with zarith. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType