proposition: Lemma spec_double_to_Z : forall n (x:word w n), 0 <= [!n | x!] < double_wB n.
proof: Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. induction n;intros. exact (spec_to_Z x). unfold double_to_Z;fold double_to_Z. destruct x;unfold zn2z_to_Z. unfold double_wB,base;split;auto with zarith. assert (U0:= IHn w0);assert (U1:= IHn w1). split;auto with zarith. apply Z.lt_le_trans with ((double_wB n - 1) * double_wB n + double_wB n). assert (double_to_Z n w0*double_wB n <= (double_wB n - 1)*double_wB n). apply Z.mul_le_mono_nonneg_r;auto with zarith. auto with zarith. rewrite <- double_wB_wwB. replace ((double_wB n - 1) * double_wB n + double_wB n) with (double_wB n * double_wB n); [auto with zarith | ring]. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType