Working on minimal mem supporting lemmas, dead ended temp. looking at functions for direct approach...

So basically... I've got all this supporting stuff now in util.v that
allows me to talk about the transitive closure of a Relation as a list.
They're proven to be equivalent.

I made some lemmas based on this that lead up to minimal member. I've
proven two of the four supporting lemmas and am now trying to prove
that if we know there is a reverse path from a given node (and we know
it is finite length and bounded by the size of the set of nodes) then
there is some reverse path from that node which is greater than or
equal to in length to all other paths from that node. So again, I'm
trying to prove an existence... I'm concerned I'm merely kicking this
existence can around into existences that are easier to fathom rather
than really breaking it apart and conquering it.

To prove this longest list/path lemma (strands3.v, L1325,
"rev_tpath_max_len"), I'm starting to think I either need to define
some functions that actually builds the dang thing and then prove
properties about it, or I could try and build the set of all the
possible lists and inductively reason on that set (that it must contain
a longest list). Both sound like a pain, the former less so... but wait
a minute. If I'm writing a function that builds the longest possible
reverse path and then I have to prove it *is* actually building the
path that is the longest, aren't I just manually backtracking to find
the minimal node??? So then what the hell benefit has there been to all
of this rewording/rephrasing/simplifying if I'm just, in the end,
manually building a function that backtracks from node to node till it
dead ends. Why bother with the rewording. Why not just make a function
called "get _minimal_node" that takes a node and backtracks till it
can't any more and prove it in fact just found a minimal node in this
set.

I don't know - maybe I'm just frustrated and not entirely thinking
clearly... but I've been wondering to myself today if anytime I'm
trying to prove "exists..." if I shouldn't just immediately start
looking for Definition and Fixpoint functions which can get me towards
that existence rather than trying to think about it from some super
high level math perspective and reason about why it is true. Maybe I
should start trying to solve these existence proofs in Racket and
convert them into Coq rather than building supporting lemmas...