[SimpleGraph/Acyclic] Add IsTrail versions of acyclic theorems #39
Description
isAcyclic_iff_path_unique, isTree_iff_existsUnique_path, IsTree.existsUnique_path talk about unique paths, but they should still hold for unique trails. It's useful for some directions.
Also prove: G.IsAcyclic ↔ ∀ (u v : V) (p : G.Walk u v), p.IsPath ↔ p.IsTrail