proposition: Theorem Zdiv_shift_r: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> (r * 2 ^a + t) / (2 ^ b) = (r * 2 ^a) / (2 ^ b).
proof: Proof. intros a b r t (H1, H2) H3 (H4, H5). assert (Eq: t < 2 ^ b); auto with zarith. apply Z.lt_le_trans with (1 := H5); auto with zarith. apply Zpower_le_monotone; auto with zarith. pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq_full with (b := 2 ^ b); auto with zarith. rewrite <- Z.add_assoc. rewrite <- Zmod_shift_r; auto with zarith. rewrite (Z.mul_comm (2 ^ b)); rewrite Z_div_plus_full_l; auto with zarith. rewrite (fun x y => @Zdiv_small (x mod y)); auto with zarith. match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; auto with zarith. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia