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:20:19 +0100

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.

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