Lemmas about (finite domain) functions into fields. #
We split this from Algebra.Order.Field.Basic to avoid importing the finiteness hierarchy there.
theorem
Pi.exists_forall_pos_add_lt
{α : Type u_1}
{ι : Type u_2}
[LinearOrderedCancelAddCommMonoid α]
[Nontrivial α]
[DenselyOrdered α]
[ExistsAddOfLE α]
[Finite ι]
{x : ι → α}
{y : ι → α}
(h : ∀ (i : ι), x i < y i)
: