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) : ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i