The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 writes:

> You may have to prove that all proofs of m < n are equal, to ensure that f
> and g do not base their decisions merely on difference in the proof parts
> of their inputs.
> Without axioms, proving this may be tricky at best, or may not even hold.

See lt_irrelevance here [1] for a proof.

> So, you can instead have f and g be of type nat - > nat. You can instead
> modify your lemma minimal_exists to express that you are only interested in
> inputs smaller than some number.

A proof iterating over a nat may be a bit tricky, you may need methods
similar to the proof of countable choice which IMHO are not exactly
straightforward (specially for the beginner).

An easier approach may be to perform a direct exhaustive search for the
minimum over the finite list of elements of the ordinal.

E.

[1] 
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v#L416