Commit 2026-10-20 12:09 4cc3c27e

feat(Combinatorics/SimpleGraph/Paths): add lemma about the first dart if dropLast is a path (#40963) If dropLast of a walk is a path, a dart of the walk sharing its first vertex with the walk also shares its second vertex. I thought this was a natural more general form of IsPath.eq_snd_of_mem_edges, useful for cycles for example.