Two non-equal lists must differ somewhere

Stream: new members

[Martin Dvořák]

PROVE:
"If we have two non-equal lists of the same length, they must have a position where they differ."

I expect a similar lemma to already exist but it probably has a different formulation. There too many ways how I could formulate it, so library_search was of no help.

example (x y : list ℕ) (same_len : x.length = y.length) (hyp : x ≠ y) :
  ∃ n : ℕ, ∃ hx : n < x.length, ∃ hy : n < y.length,
    x.nth_le n hx ≠ y.nth_le n hy :=
begin
  sorry
end

[Alex J. Best]

This looks like the negation of docs#list.ext_le