The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

the problem comes from the fact that you are using pairing.
You then need to tell Coq explicitly that
m <= n is the same than (fun p => snd p <= fst p) (n,m)
so that induction proceeds as expected:

Here it goes:

Require Omega.

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.
intros n m H; change ((fun p => snd p <= fst p) (n,m)).
elim H; simpl; intros; omega.
Qed.

--
Laurent