X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FNLE%2Ffwd.ma;h=5ddeb41aff1b1efe28b47c639310f49cd8373f50;hb=c99cecf223de21ed2ebb32106d661ce8b4dac9a8;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..5ddeb41af 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -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.