The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

For this case you may find this file interesting:

theories/Logic/ConstructiveEpsilon.v

JFM

On Thu, Nov 26, 2015 at 05:34:25PM +0100, Pierre-Marie Pédrot wrote:
> 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)
> 
> PMP