  We describe a dataset expressing and proving properties of graph trails,
using Isabelle/HOL. We formalize the reasoning about strictly increasing and
decreasing trails, using weights over edges, and prove lower bounds over the
length of trails in weighted graphs. We do so by extending the graph theory
library of Isabelle/HOL with an algorithm computing the length of a longest
strictly decreasing graph trail starting from a vertex for a given weight
distribution, and prove that any decreasing trail is also an increasing one.
  This preprint has been accepted for publication at CICM 2020.
