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 n p a H. rewrite Zmod_small. - rewrite Zmod_eq by auto with zarith. unfold Zminus at 1. rewrite Zdiv.Z_div_plus_full_l by auto with zarith. replace (2 ^ n) with (2 ^ (n - p) * 2 ^ p) by (rewrite <- Zpower_exp; [ f_equal | | ]; lia). rewrite <- Zdiv_Zdiv, Z_div_mult by auto with zarith. rewrite (Zmult_comm (2^(n-p))), Zmult_assoc. rewrite Zopp_mult_distr_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. generalize (pow2_pos (n - p)); nia. Qed.
imports: CyclicAxioms ZArith Uint63