The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I tried to make function (?) that's transforming proof of m<=n to proof of (pred m)<=n.

My try was:

Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.

Proof.

 destruct m. assumption. simpl. apply le_S_n. inversion p; auto.

Qed.

But it always gives proof of (pred m)<=n. For example, proof of 3<=14 is transformed to (pred 3)<=14. I don't know how to simplify it to 2<=14 (using the same function).

Is it possible?