proposition: Theorem spec_shiftr_pow2 : forall x n, [shiftr x n] = [x] / 2 ^ [n].
proof: Proof. intros x y. rewrite shiftr_fold. apply spec_same_level. clear x y. intros n x p. simpl. assert (Hx := ZnZ.spec_to_Z x). assert (Hy := ZnZ.spec_to_Z p). generalize (ZnZ.spec_sub_c (ZnZ.zdigits (dom_op n)) p). destruct ZnZ.sub_c as [d|d]; intros H; unfold interp_carry in *; simpl. rewrite spec_reduce. rewrite ZnZ.spec_zdigits in H. rewrite ZnZ.spec_add_mul_div by auto with zarith. rewrite ZnZ.spec_0, Z.mul_0_l, Z.add_0_l. rewrite Zmod_small. f_equal. f_equal. auto with zarith. split. auto with zarith. apply div_pow2_bound; auto with zarith. rewrite ZnZ.spec_0. symmetry. apply Zdiv_small. split; auto with zarith. apply Z.lt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith. unfold base. apply Z.pow_le_mono_r; auto with zarith. rewrite ZnZ.spec_zdigits in H. generalize (ZnZ.spec_to_Z d); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen