proposition: Theorem w_lsr_n_spec: forall w, [|w|] < 2 ^ [|n|] * [|b|]-> [|w_lsr_n w|] = [|w|] / 2 ^ [|n|].
proof: Proof. intros w2 H. case (ZnZ.spec_to_Z w2); intros U1 U2. unfold w_lsr_n, w_add_mul_div. rewrite ZnZ.spec_add_mul_div. rewrite _w0_is_0; rewrite Zmult_0_l. rewrite Zplus_0_l. autorewrite with w_rewrite. rewrite (fun x y => Zmod_small (x - y)). unfold w_zdigits; rewrite ZnZ.spec_zdigits. assert (tmp: forall p q, p - (p - q) = q) by (intros; ring). rewrite tmp; clear tmp. rewrite Zmod_small. reflexivity. split. auto with zarith. apply Z.le_lt_trans with (2 := U2). apply Zdiv_le_upper_bound. auto with zarith. apply Z.le_trans with ([|w2|] * (2 ^ 0)). simpl Zpower; rewrite Zmult_1_r; reflexivity. apply Zmult_le_compat_l. 2: auto with zarith. apply Zpower_le_monotone; auto with zarith. case (ZnZ.spec_to_Z n); auto with zarith. unfold n. assert (HH: 0 < [|b|]) by auto with zarith. split. case (Zle_or_lt [|w_head0 b|] [|w_zdigits|]); auto with zarith. unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto; intros H1. case (ZnZ.spec_head0 b HH); intros _ H2; contradict H2. apply Zle_not_lt; unfold base. apply Z.le_trans with (2^[|ZnZ.head0 b|] * 1); auto with zarith. rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. apply Z.le_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. case (ZnZ.spec_to_Z (w_head0 b)); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. autorewrite with w_rewrite; auto. rewrite Zmod_small; auto with zarith. unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto with zarith. case (ZnZ.spec_to_Z n); auto with zarith. unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. split; auto with zarith. case (Zle_or_lt [|n|] (Zpos (ZnZ.digits w_op))); auto with zarith; intros H1. case (ZnZ.spec_head0 b); auto with zarith; intros _ H2. contradict H2; apply Zle_not_lt; auto with zarith. unfold base; apply Z.le_trans with (2 ^ [|ZnZ.head0 b|] * 1); auto with zarith. rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith. apply Z.le_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. case (ZnZ.spec_to_Z n); auto with zarith. unfold base; apply Zpower2_lt_lin; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux