X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FNLE%2Ffwd.ma;h=afefbfd4db919ed53eea720b2dc927d4047555e0;hb=d748e568acf1aaf82b63b6f703d131fcc4a3c994;hp=f61fadfeee5f2b42b24b73aeca5b037c1e6af0be;hpb=07e176d2d2355cea8c5b9990cbbc3c7d234bfe15;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
index f61fadfee..afefbfd4d 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -25,7 +25,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to
  intros. decompose.
  lapply linear nplus_gen_succ_2 to H1 as H.
  decompose. subst.
- apply ex_intro; auto. (**)
+ apply ex_intro;[| auto] (**)
 qed.
 
 
@@ -36,16 +36,16 @@ theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
  auto.
 qed.
 
-theorem nle_gen_succ_zero: \forall (P:Prop). \forall x. x < zero \to P.
+theorem nle_gen_succ_zero: \forall x. x < zero \to False.
  intros.
  lapply linear nle_gen_succ_1 to H. decompose.
- apply (eq_gen_zero_succ ? ? H1).
+ lapply linear eq_gen_zero_succ to H1. decompose.
 qed.
 
 theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
  intros 1. elim x; clear x; intros;
  [ auto new timeout=30
- | apply (nle_gen_succ_zero ? ? H1)
+ | lapply linear nle_gen_succ_zero to H1. decompose.
  ].
 qed.