proposition: Lemma mod_pow2_same_cases: forall a n, a mod 2 ^ n = a -> 2 ^ n = 0 \/ 0 <= a < 2 ^ n.
proof: Proof. intros. assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C]. - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto. - right. rewrite <- H. apply Z.mod_pos_bound. apply Z.pow_pos_nonneg; lia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith