proposition: Lemma exp2_k_mult_pos k: (0 < k -> 4 <= exp2 k * (k + 2))%nat.
proof: Proof. change 4 with (2 * 2)%nat; intro Hk; apply Nat.mul_le_mono; auto. - generalize (exp2_ge_S k); abstract lia. - abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)