The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 11/26/2015 05:34 PM, Pierre-Marie Pédrot wrote:

> I don't think that this is intuitionistically provable when P is not
> decidable though. Note that relying on such proof techniques (« let n be
> the smallest integer s.t. ... ») smells a lot like you're trying to
> reason classically.

Or maybe he can replace his argument with a proof by well-founded
induction over lt (< on nat) ? And this wouldn't require decidability
of P.

D.