proposition: Lemma fun_le_trans f g h : f <<= g -> g <<= h -> f <<= h.
proof: Proof. intros; red; intro n; transitivity (g n); auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)