The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Note that `omega` has been deprecated since Coq 8.12, so better use 
`lia` instead.

https://coq.github.io/doc/master/refman/changes.html#version-8-12

On 22/12/2020 21.21, Adam Chlipala wrote:
> It's certainly a good exercise to learn how to work with "le" proofs in 
> a more fundamental way, but your example falls within linear arithmetic, 
> a decidable theory, so there is a very simple proof.
>
> Require Import Omega.
>
> Theorem le_to_exist : forall n m,
>      S n <= m
>      -> exists k, S k + n = m.
> Proof.
>    intros.
>    exists (m - S n).
>    omega.
> Qed.
>
> On 12/22/20 3:16 PM, Patricia Peratto wrote:
> > I want to prove:
> >
> >
> > Theorem le_to_exist (n m:nat)(p:le (S n) m):
> > exists_prop nat
> > (fun (k:nat)=>add (S k) n = m).
> >
> >
> > Patricia
> > ------------------------------------------------------------------------
> > *De: *"Patricia Peratto" <psperatto AT vera.com.uy>
> > *Para: *"coq-club" <coq-club AT inria.fr>
> > *Enviados: *Martes, 22 de Diciembre 2020 17:04:08
> > *Asunto: *[Coq-Club] cases in leq proof
> >
> > Is there some way to make a case analisis over a proof
> > of a leq proposition?
> >
> > Regards,
> > Patricia