coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] OASIS for Coq?

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Bas Spitters <spitters AT cs.ru.nl>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] OASIS for Coq?
Date: Thu, 3 Feb 2011 07:27:17 +0100

Here is a slight improvement, although it looks more like a doggy to me.

Theorem Bas_has_a_pony:

    forall                    b a s,
     exists                 p, exists o,
      exists                n, exists y,
      p + o + n + y >= b + a + s.
       Proof. intros. exists 0.
       exists b.      exists a.
       exists          s. auto.

Qed.

With kind regards,

Andrej

[Coq-Club] OASIS for Coq?, Bas Spitters
- Re: [Coq-Club] OASIS for Coq?, Andrej Bauer
  - Re: [Coq-Club] OASIS for Coq?, Andrej Bauer