Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: "gallais @ EnsL" <guillaume.allais AT ens-lyon.fr>
  • To: St�phane Glondu <steph AT glondu.net>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Easy proofs complicated with reals
  • Date: Sat, 28 Aug 2010 12:16:28 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=NvmwxOlCiqOi1vpcNp/5rFMaJaCVEy+WCKqc8XBYjyKNxodc6xNj6QS+J9BGjlgvdS LWFS5/rA5URSoQIH2WCfty7dXna1bBGSfnETIXBHKjJXt2gNhu0UqgwUu0gqEzq0ScfU JUkLjFSRt9zay7pVWQIAhvugtql/1VDWX9AqY=
Hi Stéphane,

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

Cheers,
--
guillaume



On 27 August 2010 18:00, Stéphane Glondu 
<steph AT glondu.net>
 wrote:
>
> SearchAbout is absolutely needed to find lemmas in the stdlib (there are
> so many of them about reals...) The first lemma looks like it should be
> part of the standard library, but I didn't find it...
>
>
> Cheers,
>
> --
> Stéphane


Archive powered by MhonArc 2.6.16.

Top of Page