refactoring

[helm.git] / helm / software / matita / contribs / RELATIONAL / NLE / fwd.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
index f61fadfeee5f2b42b24b73aeca5b037c1e6af0be..afefbfd4db919ed53eea720b2dc927d4047555e0 100644 (file)
--- 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.