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 (max i j); eapply dominates_from_max with g; eauto. Qed.
imports: Coq(ArithRing Lia Arith)