X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FRELATIONAL%2FNLE%2Fdec.ma;h=918acfe53e25a93d459e91298d5f9bb332299564;hb=ac7831c825d6c3227053f3e339a53b10e3e7118f;hp=7c45ab488d45897055e31cea808baec2afae5587;hpb=30bc693172eccfcd1440aef51e3e7c5f4171ef67;p=helm.git

diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma
index 7c45ab488..918acfe53 100644
--- a/matita/contribs/RELATIONAL/NLE/dec.ma
+++ b/matita/contribs/RELATIONAL/NLE/dec.ma
@@ -18,12 +18,12 @@ include "NLE/props.ma".
 
 theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  intros 2; elim y; clear y;
- [ auto new timeout=100
+ [ auto
  | decompose;
-   [ lapply linear nle_gen_succ_1 to H1. decompose.
-     subst. auto new timeout=100 depth=4
+   [ lapply linear nle_inv_succ_1 to H1. decompose.
+     subst. auto depth=4
    | lapply linear nle_lt_or_eq to H1; decompose;
-     subst; auto new timeout=100
+     subst; auto
    ]
  ].
 qed.