The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  I don't understand what you want exactly to get.
  By Coq's typing rules, a proof of pred 3 <= 14 is ***already*** a  
proof of 2 <=14.

Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
Proof.
 destruct m. assumption. simpl. apply le_S_n. inversion p; auto.
Qed.


Require Import Arith.

Example E1 : 3 <= 14.
auto with arith. Qed.

Check ttt _ _ E1 : 2 <= 14.



Pierre



Quoting 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?