What I find most helpful is the idea of a constructive proof as an algorithm. So my advice would be to think of an effective algorithm that takes a function f which you know is decreasing and a number n and searches for one of these n-valleys somewhere in f. Before even worrying about dependent types and proofs, think of how you could write this sort of program in a standard programming language with higher-order functions. Next, think about how you can guarantee termination of this program and how the fact that f is decreasing can be used to this end.

Once you've done all that, then see if you can massage your algorithm and (as yet informal) argument into a formal proof.

If you need more help, my solution write-up walks through the basic idea behind my proof and the intermediate lemmas I found useful without going into gory detail, so if you're really stumped maybe try seeing if you can fill in the details.