The Coq mailing list

["gallais @ EnsL.org" <guillaume.allais AT ens-lyon.org>]

Hi Tie,

How about rewriting Zcompare_Eq_iff_eq in your hypothesis and then
rewrite / destruct it?

Cheers,

--
gallais



On 17 February 2011 22:31, Tie Cheng 
<chengtie AT gmail.com>
 wrote:
> Hello Viktor,
> Thanks for your reply.
> If I do "apply Zcompare_Eq_eq", it changes the goal to "(a * something
> ?=0)%Z = Eq" which is not what I want. I want the goal to be "(0 *
> something)%Z = 0%Z". Is there a better way to use Zcompare_Eq_eq?
> Regards
> Tie
>
> On Thu, Feb 17, 2011 at 9:25 PM, Viktor Vafeiadis 
>Â <viktor AT mpi-sws.org>
> wrote:
>>
>> Second lemma in Zcompare standard library.
>> Zcompare_Eq_eq
>>
>>
>> On 17 Feb 2011, at 21:20, Tie Cheng 
>>Â <chengtie AT gmail.com>
>>  wrote:
>>
>> > hello all,
>> >
>> > I have a hypothesis "e: (a ?=0)%Z = Eq", my goal is " (a * something)%Z
>> > = 0%Z".
>> >
>> > Does anyone know how I could use the hypothesis? Is there a lemma to say
>> > "(a ?=0)%Z = Eq -> a=0%Z"?
>> >
>> > Thanks and regards
>> >
>> > Tie
>
>