Theorem: Matrix.rightConcat_last (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
α✝ : Type u_1
s : Fin n → α✝
a : α✝
⊢ (s <: a) (last n) = a
Tactic:
simp[vecConsLast]
State after:
no goals