proposition: Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.
proof: Proof. intros a b r t ? ? ?. replace (2^b) with (2^a * 2^(b-a)) by (rewrite <-Zpower_exp; [f_equal| |]; lia). assert (0 < 2 ^ (b - a)) by (apply Z.pow_pos_nonneg; lia). rewrite Z.add_mul_mod_distr_l, <- Z.mul_mod_distr_l; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63