coq-club AT inria.fr

Subject: The Coq mailing list

List archive

chronological Thread

From: Tie Cheng <chengtie AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq"
Date: Thu, 17 Feb 2011 21:20:12 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=BtZkXlzWSxehg4x6AlZjtY4d1gDMeHjAYAN+DaqRUJ3BXuqYWb1qmGS+T/RU57sMyb JtOz+pUYr4487qevwelSy3fOmUb1jv6WXUxkKfFxAndVJ5RGyjjU9Go1HakSZmZDzlT5 mhRR9gEkXFEfO2sOPnCuLz46lgPAak5tQ1hdo=

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

[Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng
- Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Viktor Vafeiadis
  - Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng
    - Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", gallais @ EnsL.org
    - Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", St�phane Lescuyer
      - Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq", Tie Cheng