no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ n + 1 ≤ ↑j + (q + 1)
simpa only [← add_assoc] using le_add_right hj