α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, t ++ l = replicate (n - length l) a ++ l
α : Type u_1
n : Nat
a : α
l : List α
⊢ l <:+ leftpad n a l
simp only [isSuffix, leftpad]
no goals
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, t ++ l = replicate (n - length l) a ++ l
exact Exists.intro (replicate (n - length l) a) rfl