proposition: Lemma shift_unshift_mod : forall n p a, 0 <= a < 2^n -> 0 <= p <= n -> a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n.
proof: Proof. intros n p a H1 H2. pattern (a*2^p) at 1;replace (a*2^p) with (a*2^p/2^n * 2^n + a*2^p mod 2^n). 2:symmetry;rewrite (Z.mul_comm (a*2^p/2^n));apply Z_div_mod_eq_full. replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial. replace (2^n) with (2^(n-p)*2^p). symmetry;apply Zdiv_mult_cancel_r. destruct H1;trivial. cut (0 < 2^p); auto with zarith. rewrite <- Zpower_exp. replace (n-p+p) with n;trivial. ring. lia. lia. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia