no goals
α : Type u_1
β : Type ?u.28972
m : Type u_2
n : Type ?u.28978
o : Type ?u.28981
m' : α → Type ?u.28986
n' : α → Type ?u.28991
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.add_apply, hM h, hN h, zero_add]