The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

On 11/8/06, Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 wrote:
> Given the simple inductive definition here, I would like to prove the
> simple lemma below it.
>
> Inductive foo : nat * nat -> Prop :=
> | foo1 : forall i j k, i = j + k -> foo (i, j)
> | foo2 : forall i j k, foo (i, j + k) -> foo (i, j).
>
> Lemma bar : forall n m, foo (n, m) -> m <= n.

Thanks for the helpful responses.  I find the use of the "change"
tactic especially elegant.  However, it does not seem applicaple to
the slightly more general case where I would like to prove:

Lemma bar : forall n m p, foo (n, m + p) -> m <= n.

Am I correct in assuming that I need to take one of the longer
approaches when dealing with a lemma like this?

-Aaron