The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Serge Leblanc 
<serge.leblanc AT wanadoo.fr>:

> 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
>

Hi,

 There is a solution (attached) (with some non-trivial feature : the caseEq
tactic)
Perhaps one can give a simpler solution ???

Pierre





-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Attachment: Zmin.v
Description: Binary data