coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Beginnier question.

From: Serge Leblanc <serge.leblanc AT wanadoo.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Beginnier question.
Date: Fri, 20 May 2005 19:13:56 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I am trying to prove the the following trivial goal. I don't reach it, can you show me how to make?

Goal forall n m:Z, Zmin n m = Zmin m n.

Sincerely,

Serge Leblanc <serge.leblanc AT wanadoo.fr> GnuPG id: 1024D/73791C2B 2002-09-30 
Primary key fingerprint: 8E0C 0D6D E026 A278 9278  BF4F 1A93 D552 7379 1C2B

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Beginnier question., Serge Leblanc
- Re: [Coq-Club] Beginnier question., Pierre Casteran
  - Re: [Coq-Club] Beginnier question., Pierre Courtieu
- Re: [Coq-Club] Beginnier question, Pierre Casteran
- Re: [Coq-Club] Beginnier question., Roland Zumkeller
- Re: [Coq-Club] Beginnier question., Serge Leblanc
  - Re: [Coq-Club] Beginnier question., Pierre Casteran
    - Re: [Coq-Club] Beginnier question., roconnor
- Re: [Coq-Club] Beginnier question., David Pichardie
  - [Coq-Club] Rational numbers, Carlos.SIMPSON