proposition: Lemma dominates_trans : forall f g h, dominates g f -> dominates h g -> dominates 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)