proposition: Lemma dominates_trans_strong : forall f g h, dominates_strong g f -> dominates_strong h g -> dominates_strong h f.
proof: Proof. intros f g h [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)