∀ {α : Type u_1} [inst : LT α] [i₁ : Std.Asymm fun x1 x2 => x1 < x2] [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2]
  [i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {xs ys zs : Array α},
  xs ≤ ys → ys < zs → xs < zs