proposition: Lemma exp2_as_iterate n : exp2 n = iterate (fun i => 2 * i)%nat n 1.
proof: Proof. induction n. - reflexivity. - rewrite iterate_S_eqn; simpl exp2; rewrite <- IHn; abstract lia. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)