The Coq mailing list

[Xingyuan Zhang <Xingyuan.Zhang AT durham.ac.uk>]

Hi,
The following is a proof in which Fix and Inversion are used together:

Lemma lt_O_ex : (n:nat)(lt O n)->(EX m:nat | n = (S m)).
Fix mf 2.
Intros.
Inversion H.
Show Proof.
Exists O.
Auto.
Show Proof.
Generalize (mf ? H0).
Show Proof.
Intros (m0, eq_m).
Show Proof.
Rewrite eq_m.
Exists (S m0).
Auto.
Show Proof.
Save.

The final proof term is rejected by Coq for not satisfying the guarded 
condition. However, intuition told me that the recursive application of ma 
is really applied to something "smaller". My question is:
Is it in general acceptable that the recursive function is applied to an 
arguments which are result of the Inversion command, or there should be 
some additional conditions for this?

Thanks!

Xingyuan Zhang