proposition: Lemma dominates_from_le i j g f : i <= j -> dominates_from i g f -> dominates_from j g f .
proof: Proof. induction 1; auto. intros H0 x H1; apply IHle; auto. auto with arith. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)