coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]induction proof

From: "Carlos.SIMPSON" <carlos AT math.unice.fr>
To: Pierre Casteran <pierre.casteran AT labri.fr>
Cc: topwl AT free.fr, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]induction proof
Date: Fri, 12 May 2006 08:45:28 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Require Arith.
Require Omega.

Lemma lt_plus_ab : forall n a b : nat, n < a + b ->
n < a \/ exists y, n=a+y /\ y < b.
Proof.
intros.
assert (n< a \/ n>= a).
omega.
induction H0.
apply or_introl. assumption.
apply or_intror.
apply ex_intro with (n-a).
apply conj.
omega. omega.
Qed.

Conclusion: omega is great, we need more tactics like that!
---Carlos Simpson

[Coq-Club]induction proof, topwl
- Re: [Coq-Club]induction proof, Pierre Casteran
  - Re: [Coq-Club]induction proof, Pierre Casteran
    - Re: [Coq-Club]induction proof, Carlos.SIMPSON
- Re: [Coq-Club]induction proof, Jean.Duprat