α : Type u_1
a : α
l : List α
i : Nat
h : i = length l
⊢ get? (reverse (a :: l)) i = get? (a :: l) 0
α : Type u_1
a : α
l : List α
i : Nat
h : i + 0 + 1 = length (a :: l)
⊢ get? (reverse (a :: l)) i = get? (a :: l) 0
simp at h
no goals
α : Type u_1
a : α
l : List α
i : Nat
h : i = length l
⊢ get? (reverse (a :: l)) i = get? (a :: l) 0
simp [h, get?_append_right]
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ get? (reverse (a :: l)) i = get? (a :: l) (j + 1)
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
⊢ get? (reverse (a :: l)) i = get? (a :: l) (j + 1)
have := Nat.succ.inj h
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ get? (reverse l ++ [a]) i = get? l j
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ get? (reverse (a :: l)) i = get? (a :: l) (j + 1)
simp at this ⊢
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ i < length (reverse l)
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ get? (reverse l ++ [a]) i = get? l j
rw [get?_append, get?_reverse' _ j this]
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ i < i + (j + 1)
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ i < length (reverse l)
rw [length_reverse, ← this]
no goals
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = length (a :: l)
this : i + (j + 1) = length l
⊢ i < i + (j + 1)
apply Nat.lt_add_of_pos_right (Nat.succ_pos _)