proposition: Theorem spec_double_size_head0: forall x, 2 * [head0 x] <= [head0 (double_size x)].
proof: Proof. intros x. assert (F1:= spec_pos (head0 x)). assert (F2: 0 < Zpos (digits x)). red; auto. assert (HH := spec_pos x). Z.le_elim HH. generalize HH; rewrite <- (spec_double_size x); intros HH1. case (spec_head0 x HH); intros _ HH2. case (spec_head0 _ HH1). rewrite (spec_double_size x); rewrite (spec_double_size_digits x). intros HH3 _. case (Z.le_gt_cases ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4. absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto. apply Z.le_ngt. apply Z.mul_le_mono_nonneg_r; auto with zarith. apply Z.pow_le_mono_r; auto; auto with zarith. assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)). { apply Z.le_succ_l in HH. change (1 <= [x]) in HH. Z.le_elim HH. - apply Z.mul_le_mono_pos_r with (2 ^ 1); auto with zarith. rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith. rewrite Z.sub_add. apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2). apply Z.mul_le_mono_nonneg_l. auto with zarith. rewrite Z.pow_1_r; auto with zarith. - apply Z.pow_le_mono_r; auto with zarith. case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6. absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith. rewrite <- HH; rewrite Z.mul_1_r. apply Z.pow_le_mono_r; auto with zarith. } rewrite (Z.mul_comm 2). rewrite Z.pow_mul_r by auto with zarith. rewrite Z.pow_2_r. apply Z.lt_le_trans with (2 := HH3). rewrite <- Z.mul_assoc. replace (2 * Zpos (digits x) - 1) with ((Zpos (digits x) - 1) + (Zpos (digits x))). rewrite Zpower_exp by auto with zarith. apply Zmult_lt_compat2; [auto with zarith|]. - split;[|auto with zarith]. apply Z.mul_pos_pos; auto with zarith. - rewrite Pos2Z.inj_xO; ring. - apply Z.lt_le_incl; auto. - repeat rewrite spec_head00; auto. rewrite spec_double_size_digits. rewrite Pos2Z.inj_xO; auto with zarith. rewrite spec_double_size; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen