(Thanks for these problem sets, which I've been very much enjoying as I learn Coq.)

In Pset3, the two monotonicity-related theorems are degenerate in the following sense:

bst_strict_monotone_increasing: Under the assumptions of the theorem, namely that f : nat -> nat has a right inverse and is strictly monotone, we can prove f = id. This makes the theorem trivial.

bst_strict_monotone_decreasing_mirror: The theorem assumes that f : nat -> nat is strictly decreasing, but there is no such function. Thus the theorem can be proven by showing that the hypotheses are contradictory.

I assume this is just an accident caused by using nat for convenience, since various other totally-ordered sets (such as the integers or the rationals) wouldn't have this problem.

(Edit: Fixed accidentally saying f has a left inverse. f has a right inverse, because the left inverse of g is f. The important thing is that it causes f to be onto.)