diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean
index 0777097210edb8..c69283b93515a1 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean
@@ -381,6 +381,8 @@ lemma not_nil_iff {p : G.Walk v w} :
 lemma nil_iff_eq_nil : ∀ {p : G.Walk v v}, p.Nil ↔ p = nil
   | .nil | .cons _ _ => by simp
 
+lemma not_nil_iff_ne_nil {p : G.Walk v v} : ¬ p.Nil ↔ p ≠ nil := by rw [nil_iff_eq_nil]
+
 alias ⟨Nil.eq_nil, _⟩ := nil_iff_eq_nil
 
 lemma nil_of_subsingleton [Subsingleton V] (p : G.Walk v w) : p.Nil :=