Connection between list.nth and list.nth_le

Stream: new members

[Martin Dvořák]

Without further ado, I am stuck on:

example (T : Type) (lis : list T) (n : ℕ) (hn : n < lis.length) (val : T) (h : lis.nth_le n hn = val) :
  lis.nth n = some val :=
begin
  sorry,
end

[Eric Wieser]

rw ←h seems like the obvious start