The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi Guillaume,

That´s not the case, but thanks anyway for sharing your code.

Best Regards,

Marcus.

2014-07-23 9:39 GMT-03:00 gallais <guillaume.allais AT ens-lyon.fr>:

Hi Marcus,

If you use symmetry on inequalities quite a lot in your proof scripts,
you should probably define a wee module making [symmetry] work for [<>].

Here is the way we've done it in Coqtail:
https://github.com/coqtail/coqtail/blob/master/src/mytheories/MyNeq.v

Cheers,
gallais

On 22/07/14 21:46, Marcus Ramos wrote:

​Hi,

My goal is "l <> []"​, however I need it to be "[] <> l". How can I get
this since symmetry does not work for <>?

Thanks,
Marcus.