proposition: Lemma shift_unshift_mod_3: forall n p a : Z, 0 <= p <= n -> (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) = a mod 2 ^ p.
proof: Proof. intros;rewrite <- (shift_unshift_mod_2 n p a);[ | auto with zarith]. symmetry;apply Zmod_small. generalize (a * 2 ^ (n - p));intros w. generalize (2 ^ (n - p)) (pow2_pos (n - p)); intros x; apply P. - lia. - intros hx. generalize (2 ^ n) (pow2_pos n); intros y; apply P. + lia. + intros hy. elim_div. intros q r. apply P. * lia. * elim_div. intros z t. refine (P _ _ _ _ _). -- lia. -- intros [ ? [ ht | ] ]; [ | lia ]; subst w. intros [ ? [ hr | ] ]; [ | lia ]; subst t. nia. Qed.
imports: CyclicAxioms ZArith Uint63