arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_lt_minus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
index 5ee4b80eb03427110a773454718d101e8751e579..bf889def7538d99a54e5f9f7e360ebb195260abc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
@@ -38,7 +38,7 @@ qed.
 
 (* Destructions with nminus *************************************************)
 
-lemma nlt_fwd_minus_dx (o) (m) (n): m < n - o → o < n.
+lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
 #o elim o -o
 [ #m #n <nminus_zero_dx
   /2 width=3 by le_nlt_trans/