feat(Combinatorics/SimpleGraph/Paths): p.IsPath → p.dropLast.IsPath (leanprover-community#40667)

We have this for `tail`/`take`/`drop`/`takeUntil`/`dropUntil`/`reverse`/`copy`/`concat` but not for `dropLast`.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -358,6 +358,9 @@ lemma IsPath.tail {p : G.Walk u v} (hp : p.IsPath) : p.tail.IsPath := by
   | cons hadj p =>
     simp_all [Walk.isPath_def]
 
+theorem IsPath.dropLast (hp : p.IsPath) : p.dropLast.IsPath :=
+  hp.take _
+
 /-- There exists a trail of maximal length in a non-empty graph on finite edges. -/
 lemma exists_isTrail_forall_isTrail_length_le_length (G : SimpleGraph V) [N : Nonempty V]
     [Finite G.edgeSet] :