proposition: Lemma spec_ww_head0 : forall x, 0 < [[x]] -> wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB.
proof: Proof. rewrite wwB_div_2;rewrite Z.mul_comm;rewrite wwB_wBwB. assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H. unfold Z.lt in H;discriminate H. rewrite spec_compare, spec_w_0. case Z.compare_spec; intros H0. rewrite <- H0 in *. simpl Z.add. simpl in H. case (spec_to_Z w_zdigits); case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4. rewrite spec_w_add. rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith. case (spec_w_head0 H); intros H1 H2. rewrite Z.pow_2_r; fold wB; rewrite <- Z.mul_assoc; split. apply Z.mul_le_mono_nonneg_l; auto with zarith. apply Z.mul_lt_mono_pos_l; auto with zarith. assert (H1 := spec_w_head0 H0). rewrite spec_w_0W. split. rewrite Z.mul_add_distr_l;rewrite Z.mul_assoc. apply Z.le_trans with (2 ^ [|w_head0 xh|] * [|xh|] * wB). rewrite Z.mul_comm; zarith. assert (0 <= 2 ^ [|w_head0 xh|] * [|xl|]);zarith. assert (H2:=spec_to_Z xl);apply Z.mul_nonneg_nonneg;zarith. case (spec_to_Z (w_head0 xh)); intros H2 _. generalize ([|w_head0 xh|]) H1 H2;clear H1 H2; intros p H1 H2. assert (Eq1 : 2^p < wB). rewrite <- (Z.mul_1_r (2^p));apply Z.le_lt_trans with (2^p*[|xh|]);zarith. assert (Eq2: p < Zpos w_digits). destruct (Z.le_gt_cases (Zpos w_digits) p);trivial;contradict Eq1. apply Z.le_ngt;unfold base;apply Zpower_le_monotone;zarith. assert (Zpos w_digits = p + (Zpos w_digits - p)). ring. rewrite Z.pow_2_r. unfold base at 2;rewrite H3;rewrite Zpower_exp;zarith. rewrite <- Z.mul_assoc; apply Z.mul_lt_mono_pos_l; zarith. rewrite <- (Z.add_0_r (2^(Zpos w_digits - p)*wB));apply beta_lex_inv;zarith. apply Z.mul_lt_mono_pos_r with (2 ^ p); zarith. rewrite <- Zpower_exp;zarith. rewrite Z.mul_comm;ring_simplify (Zpos w_digits - p + p);fold wB;zarith. assert (H1 := spec_to_Z xh);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase