proposition: Lemma minoration_1 : forall n x, exp2 n * x <= iterate doubleS n x.
proof: Proof. induction n; simpl. - intro; abstract lia. - intros; unfold doubleS. transitivity (2 * iterate doubleS n x). + specialize (IHn x). ring_simplify. lia. + unfold doubleS; abstract lia. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)