proposition: Theorem spec_double_size_head0_pos: forall x, 0 < [head0 (double_size x)].
proof: Proof. intros x. assert (F := Pos2Z.is_pos (digits x)). assert (F0 := spec_pos (head0 (double_size x))). Z.le_elim F0; auto. assert (F1 := spec_pos (head0 x)). Z.le_elim F1. apply Z.lt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith. assert (F3 := spec_pos x). Z.le_elim F3. generalize F3; rewrite <- (spec_double_size x); intros F4. absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))). { apply Z.le_ngt. apply Z.pow_le_mono_r. auto with zarith. rewrite Pos2Z.inj_xO; auto with zarith. } case (spec_head0 x F3). rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH. apply Z.le_lt_trans with (2 := HH). case (spec_head0 _ F4). rewrite (spec_double_size x); rewrite (spec_double_size_digits x). rewrite <- F0; rewrite Z.pow_0_r; rewrite Z.mul_1_l; auto. generalize F1; rewrite (spec_head00 _ (eq_sym F3)); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen