Ssreflect Users Discussion List

[Laurent Thery <>]

On 02/18/2016 10:32 AM, François Pottier wrote:
> Hi Enrico,
>
> > Could you check if your problem is an instance of this one?  > 
> > https://github.com/math-comp/math-comp/issues/18
>
> Apparently yes. Robert's magic line seems to fix my problems (see
> attached file). I am not sure what it does, though.
>
> What's the official doctrine regarding rewriting with inequalities
> in ssreflect? Is there a documentation or examples anywhere?
>
> Thanks,

I think it works because you are using the "old" arithmetic operators 
not the ones of ssreflect.

--
Laurent