Commit 2026-06-30 15:26 8a75b5a5
View on Github →feat(Combinatorics/SimpleGraph/Paths): some cycle lemmas are true for circuits (#38528)
Add IsCircuit.{not_of_nil,ne_bot,three_le_length} by using their corresponding IsCycle proofs.
Also golfs a bit.