proposition: Lemma spec_ww_head1 : forall x : zn2z w, (ww_is_even (ww_head1 x) = true) /\ (0 < [[x]] -> wwB / 4 <= 2 ^ [[ww_head1 x]] * [[x]] < wwB).
proof: Proof. assert (U := wB_pos w_digits). intros x; unfold ww_head1. generalize (spec_ww_is_even (ww_head0 x)); case_eq (ww_is_even (ww_head0 x)). intros HH H1; rewrite HH; split; auto. intros H2. generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10. intros (H3, H4); split. 2: zarith. apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; zarith. intros xh xl (H3, H4); split. 2: zarith. apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; zarith. intros H1. case (spec_to_w_Z (ww_head0 x)); intros Hv1 Hv2. assert (Hp0: 0 < [[ww_head0 x]]). generalize (spec_ww_is_even (ww_head0 x)); rewrite H1. generalize Hv1; case [[ww_head0 x]]. rewrite Zmod_small; zarith. intros; assert (0 < Zpos p); zarith. red; simpl; auto. intros p H2; case H2; auto. assert (Hp: [[ww_pred (ww_head0 x)]] = [[ww_head0 x]] - 1). rewrite spec_ww_pred. rewrite Zmod_small; zarith. intros H2; split. generalize (spec_ww_is_even (ww_pred (ww_head0 x))); case ww_is_even; auto. rewrite Hp. rewrite Zminus_mod by zarith. rewrite H2; repeat rewrite Zmod_small; zarith. intros H3; rewrite Hp. case (spec_ww_head0 x); auto; intros Hv3 Hv4. assert (Hu: forall u, 0 < u -> 2 * 2 ^ (u - 1) = 2 ^u). intros u Hu. pattern 2 at 1; rewrite <- Z.pow_1_r. rewrite <- Zpower_exp by zarith. ring_simplify (1 + (u - 1)); zarith. split. apply Z.mul_le_mono_pos_r with 2. zarith. repeat rewrite (fun x => Z.mul_comm x 2). rewrite wwB_4_2. rewrite Z.mul_assoc; rewrite Hu; zarith. apply Z.le_lt_trans with (2 * 2 ^ ([[ww_head0 x]] - 1) * [[x]]); rewrite Hu. 2-4: zarith. apply Z.mul_le_mono_nonneg_r. zarith. apply Zpower_le_monotone; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase