The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Balazs Vegvari wrote:
> I am just learning coq and I don't kow how to prove this:
>
> forall x y : Z, x <= y + 1 -> x <= y \/ x = y + 1
>
> Any suggestion is welcome.
>   

Did you have a particular constraint on the proof technique in mind?  
Your theorem statement falls into the theory of "quantifier-free linear 
arithmetic," which is one of the most widely-used decidable theories.  
The [omega] tactic solves it instantly (after [intros]).