proposition: Lemma pow2_div2: forall i, 0 <= i -> 2 ^ (i - 1) = 2 ^ i / 2.
proof: Proof. intros. assert (i = 0 \/ 0 < i) as C by lia. destruct C as [C | C]. - subst. reflexivity. - rewrite Z.pow_sub_r by lia. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith