The Coq mailing list

[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.