Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] two questions: a real one, and asking for help

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] two questions: a real one, and asking for help


Chronological Thread 
  • From: Clément Pit--Claudel <clement.pit AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] two questions: a real one, and asking for help
  • Date: Fri, 5 Aug 2016 05:34:57 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
  • Ironport-phdr: 9a23:as5xwhHpgiD/XUiivq3knJ1GYnF86YWxBRYc798ds5kLTJ75pMWwAkXT6L1XgUPTWs2DsrQf2rKQ4/yrATxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD14Lni6vqq9X6WEZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzoSYqK630AZV0Xjl8NKAzM8R33Wt+luS/3s+d7xG+CPNHeQrU9WDDk5KBuHky7wBwbPiI0pTmEwvd7i7hW9Uqs
On 2016-08-05 05:18, Daniel de Rauglaudre wrote:
> Hi all!

Hi Daniel,

> 1/ I don't remember the Internet tool to chat with Coq users, to ask
> simple questions. I used it once a long time ago, but I did not
> notice what I used, and I cannot find it again through google.

Could it be IRC? #coq on freenode.

> 2/ The immediate question that I have now is how to prove that the
> hypothesis (1 / 3)%R = 1%R is contradictory? I tried discriminate,
> discrR and other field_simplify. But I cannot manage to finish it
> in a simple way. A research on google gave me nothing interesting
> but perhaps I did not put the good terms.

This maybe?

Require Import Psatz.
Goal (1 / 3) = 1 -> False.
Proof.
lra.
Qed.

:)

Attachment: signature.asc
Description: OpenPGP digital signature


Archive powered by MHonArc 2.6.18.

Top of Page