proposition: Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = a mod 2 ^ p.
proof: Proof. intros. rewrite Zmod_small. rewrite Zmod_eq by (auto with zarith). unfold Z.sub at 1. rewrite Z_div_plus_l by (auto with zarith). assert (2^n = 2^(n-p)*2^p). rewrite <- Zpower_exp by (auto with zarith). replace (n-p+p) with n; auto with zarith. rewrite H0. rewrite <- Zdiv_Zdiv, Z_div_mult by (auto with zarith). rewrite (Z.mul_comm (2^(n-p))), Z.mul_assoc. rewrite <- Z.mul_opp_l. rewrite Z_div_mult by (auto with zarith). symmetry; apply Zmod_eq; auto with zarith. remember (a * 2 ^ (n - p)) as b. destruct (Z_mod_lt b (2^n)); auto with zarith. split. apply Z_div_pos; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. apply Z.lt_le_trans with (2^n); auto with zarith. rewrite <- (Z.mul_1_r (2^n)) at 1. assert (0 < 2^ (n-p)) by auto with zarith. apply Z.mul_le_mono_nonneg; auto with zarith. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia