The Coq mailing list

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

Oh, checking the file, it does not say that the witness
found by linear_search is indeed the minimum -- it is not
needed there. However I remember that it is not a big deal.
And well-foundedness of lt is not needed.

JFM

On Fri, Nov 27, 2015 at 01:07:58AM +0800, Jean-Francois Monin wrote:
> 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