Lexicographic product of algebraic order structures

This file proves that the lexicographic order on pi types is compatible with the pointwise algebraic operations.

instance Pi.Lex.isOrderedCancelMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → CommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelMonoid (α i)] : IsOrderedCancelMonoid (Lex ((i : ι) → α i))

instance Pi.Lex.isOrderedAddCancelMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)] : IsOrderedCancelAddMonoid (Lex ((i : ι) → α i))