The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 26/11/2015 17:06, David Asher wrote:
> But I need some additional information [ somethig like "~ (exists m,
> m < n /\ P m)" ] in the context. Any ideas how to solve this?

If P is decidable, you can prove by induction on n that

P n -> exists m, P m /\ (forall p, p < m -> ~ P p)

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.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature