coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq"

From: Viktor Vafeiadis <viktor AT mpi-sws.org>
To: Tie Cheng <chengtie AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] use the hypothesis "(a ?=0)%Z = Eq"
Date: Thu, 17 Feb 2011 21:25:41 +0100

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

[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