∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : CommRing R]
  [inst_2 : DecidableEq m] {i j : m}, b i ≤ b j → ∀ (c : R), (Matrix.transvection i j c).BlockTriangular b