proposition: Lemma dominates_from_max : forall f g h i j, dominates_from i g f -> dominates_from j h g -> dominates_from (max i j) h f .
proof: Proof. intros f g h i j H H0 k Hk; transitivity (g k). + apply H; eauto with arith. + apply H0; eauto with arith. Qed.
imports: Coq(ArithRing Lia Arith)