coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Easy proofs complicated with reals

From: Stéphane Glondu <steph AT glondu.net>
To: "gallais @ EnsL" <guillaume.allais AT ens-lyon.fr>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Easy proofs complicated with reals
Date: Sat, 28 Aug 2010 12:31:37 +0200
Openpgp: id=49881AD3

Le 28/08/2010 12:16, gallais @ EnsL a écrit :
> There is actually a more general lemma in the standard library (Reals >
> Rpower):
>
> Rpower_Ropp: forall x y : R, Rpower x (- y) = (/ Rpower x y)%R

But there is no direct connection between Rpower and powerRZ... is
there? All I see is going through pow... which is basically what I did
by unfolding powerRZ (but then, I don't need Rpower).

Cheers,

--
Stéphane

[Coq-Club] Easy proofs complicated with reals, Michael
- Re: [Coq-Club] Easy proofs complicated with reals, Evgeny Makarov
- <Possible follow-ups>
- Re: Re: [Coq-Club] Easy proofs complicated with reals, Michael
  - Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu
    - Re: [Coq-Club] Easy proofs complicated with reals, gallais @ EnsL
      - Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu