proposition: Lemma dominates_trans f g h : dominates g f -> dominates h g -> dominates h f.
proof: Proof. intros [i Hi] [j Hj]; exists (Nat.max i j); eapply dominates_from_trans with g; eauto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)