The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Balazs Vegvari wrote:
> one thing came into my mind after reading documentation of the omega
> tactic: what if omega could not solve a similar system, for example
> adding a nonlinear product to the example? How would I prove this
> manually in that case?
>   

I'm not sure what to say.  You are probably best off picking up the 
Coq'Art book and starting to learn about proving in Coq in general.  The 
proof techniques follow from the definitions of the identifiers you use, 
but you need to know about inductive definitions and tactics for this to 
imply a halfway effective procedure.