proposition: Lemma spec_ww_tail0 : forall x, 0 < [[x]] -> exists y, 0 <= y /\ [[x]] = (2 * y + 1) * 2 ^ [[ww_tail0 x]].
proof: Proof. 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; rewrite Z.add_0_r. case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. generalize H; rewrite <- H0; rewrite Z.add_0_r; clear H; intros H. case (@spec_w_tail0 xh). apply Z.mul_lt_mono_pos_r with wB; auto with zarith. unfold base; auto with zarith. intros z (Hz1, Hz2); exists z; split; auto. rewrite spec_w_add; rewrite (fun x => Z.add_comm [|x|]). rewrite spec_zdigits; rewrite Zpower_exp by auto with zarith. rewrite Z.mul_assoc; rewrite <- Hz2; auto. case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. case (spec_w_tail0 H0); intros z (Hz1, Hz2). assert (Hp: [|w_tail0 xl|] < Zpos w_digits). case (Z.le_gt_cases (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1. absurd (2 ^ (Zpos w_digits) <= 2 ^ [|w_tail0 xl|]). apply Z.lt_nge. case (spec_to_Z xl); intros HH3 HH4. apply Z.le_lt_trans with (2 := HH4). rewrite Hz2. apply Z.le_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith. apply Zpower_le_monotone; auto with zarith. exists ([|xh|] * (2 ^ ((Zpos w_digits - [|w_tail0 xl|]) - 1)) + z); split. apply Z.add_nonneg_nonneg; auto. apply Z.mul_nonneg_nonneg; auto with zarith. case (spec_to_Z xh); auto. rewrite spec_w_0W. rewrite (Z.mul_add_distr_l 2); rewrite <- Z.add_assoc. rewrite Z.mul_add_distr_r; rewrite <- Hz2. apply f_equal2 with (f := Z.add); auto. rewrite (Z.mul_comm 2). repeat rewrite <- Z.mul_assoc. apply f_equal2 with (f := Z.mul); auto. case (spec_to_Z (w_tail0 xl)); intros HH3 HH4. pattern 2 at 2; rewrite <- Z.pow_1_r. lazy beta; repeat rewrite <- Zpower_exp; auto with zarith. unfold base; apply f_equal with (f := Z.pow 2); auto with zarith. contradict H0; case (spec_to_Z xl); auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase