proposition: Lemma pow2_times2: forall i, 0 < i -> 2 ^ i = 2 * 2 ^ (i - 1).
proof: Proof. intros. rewrite <- Z.pow_succ_r by lia. f_equal. lia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith