proposition: Remark f_minoration n p : 0 < n -> n <= p -> exp2 n <= f p.
proof: Proof. intros ? ? ; unfold f; rewrite exp2S. pose (x := exp2 n); pose(y := exp2 p); fold x; fold y. assert (x <= y) by (now apply exp2_mono_weak). assert (2 <= S p) by lia. transitivity (2 * x * 2 - 1). - lia. - apply Nat.sub_le_mono_r. transitivity (2 * y * 2)%nat. + lia. + now apply Nat.mul_le_mono_l. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)