coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] two questions: a real one, and asking for help, Daniel de Rauglaudre, 08/05/2016
- Re: [Coq-Club] two questions: a real one, and asking for help, Laurent Thery, 08/05/2016
- Re: [Coq-Club] two questions: a real one, and asking for help, Cedric Auger, 08/05/2016
- Re: [Coq-Club] two questions: a real one, and asking for help, Clément Pit--Claudel, 08/05/2016
- Re: [Coq-Club] two questions: a real one, and asking for help, Daniel de Rauglaudre, 08/05/2016
- RE: [Coq-Club] two questions: a real one, and asking for help, Soegtrop, Michael, 08/05/2016
- Re: [Coq-Club] two questions: a real one, and asking for help, Daniel de Rauglaudre, 08/05/2016
Archive powered by MHonArc 2.6.18.