The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> On 05 Nov 2015, at 17:59, Michael Shulman 
> <shulman AT sandiego.edu>
>  wrote:
> 
> Is there a standard tactic that can automatically solve the non-zero
> conditions left over by "field", at least in simple cases?  E.g. if
> the condition is "x - 1 != 0" and we have "x != 1" as a hypothesis?
If this linear arithmetics over R, you can  try lra.

Best,
—
Frédéric

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail