no goals
α : Type u_1
β : Type ?u.29890
m : Type u_2
n : Type ?u.29896
o : Type ?u.29899
m' : α → Type ?u.29904
n' : α → Type ?u.29909
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b : m → α
inst✝ : LT α
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
h : b j < b i
⊢ (M - N) i j = 0
simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]