proposition: Lemma power2_mod : forall n m, (0 <= n -> 0 <= m -> ((2 ^ n) mod (2 ^ m) = if Z.ltb n m then 2^n else 0))%Z.
proof: Proof. intros. destruct (n <?m)%Z eqn:T. - apply Z.mod_small; auto. split. apply Z.pow_nonneg. lia. apply Z.pow_lt_mono_r; lia. - assert ((2 ^ n) = 0 + 2^(n-m) * 2^m)%Z. rewrite <- Z.pow_add_r. simpl. f_equal. lia. lia. lia. rewrite H1. rewrite Z_mod_plus_full. apply Z.mod_0_l. generalize (Z.pow_pos_nonneg 2 m). lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR