From 31bcb2d7cb6fc4c01af9d62b6ede25a9b82308aa Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 11 Nov 2006 18:53:10 +0000
Subject: [PATCH] NLE is now derived fron NPlus rather than being a stand-alone
 relation

---
 matita/contribs/RELATIONAL/NLE/defs.ma  | 16 ++++++----------
 matita/contribs/RELATIONAL/NLE/fwd.ma   | 24 +++++++++++-------------
 matita/contribs/RELATIONAL/NLE/props.ma | 17 ++++++++++++++++-
 3 files changed, 33 insertions(+), 24 deletions(-)

diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma
index 59c02653e..a9b33561d 100644
--- a/matita/contribs/RELATIONAL/NLE/defs.ma
+++ b/matita/contribs/RELATIONAL/NLE/defs.ma
@@ -14,20 +14,16 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NLE/defs".
 
-include "logic/equality.ma".
+include "NPlus/defs.ma".
 
-include "Nat/defs.ma".
-
-inductive NLE: Nat \to Nat \to Prop \def
-   | NLE_zero: \forall q. NLE zero q
-   | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q)
-.
+definition NLE: Nat \to Nat \to Prop \def
+   \lambda q,r. \exists p. (p + q == r). 
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less or equal to'" 'leq x y = 
-   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
+interpretation "natural 'less or equal to'" 'leq x y =
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.con x y).
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = 
-   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) 
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.con 
       (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index 661e00ecd..f61fadfee 100644
--- a/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -16,26 +16,24 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/fwd".
 
 include "logic/connectives.ma".
 
-include "Nat/fwd.ma". 
+include "NPlus/fwd.ma". 
 include "NLE/defs.ma".
 
 theorem nle_gen_succ_1: \forall x,y. x < y \to 
                         \exists z. y = succ z \land x <= z.
- intros. inversion H; clear H; intros;
- [ apply (eq_gen_succ_zero ? ? H)
- | lapply linear eq_gen_succ_succ to H2 as H0.
-   subst.
-   apply ex_intro; [|auto new timeout=30] (**)
- ].
+ unfold NLE. 
+ intros. decompose.
+ lapply linear nplus_gen_succ_2 to H1 as H.
+ decompose. subst.
+ apply ex_intro; auto. (**)
 qed.
 
+
 theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
- intros; inversion H; clear H; intros;
- [ apply (eq_gen_succ_zero ? ? H)
- | lapply linear eq_gen_succ_succ to H2 as H0.
-   lapply linear eq_gen_succ_succ to H3 as H2.
-   subst. auto new timeout=30
- ].
+ intros.
+ lapply linear nle_gen_succ_1 to H as H0. decompose H0.
+ lapply linear eq_gen_succ_succ to H1 as H. subst.
+ auto.
 qed.
 
 theorem nle_gen_succ_zero: \forall (P:Prop). \forall x. x < zero \to P.
diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index bd76c2754..b571dfc6b 100644
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -16,12 +16,27 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 
 include "NLE/fwd.ma".
 
+theorem nle_zero: \forall q. zero <= q.
+ unfold NLE.
+ intros. apply ex_intro; auto. (**)
+qed.
+
+theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
+ unfold NLE.
+ intros. decompose.
+ apply ex_intro; auto. (**)
+qed.
+
 theorem nle_refl: \forall x. x <= x.
  intros 1; elim x; clear x; intros; auto new timeout=100.
 qed.
 
 theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H; clear H x y; intros; auto new timeout=100.
+ intros 1. elim x; clear x; intros; 
+ [ auto new timeout=100.
+ | lapply linear nle_gen_succ_1 to H1 as H0. decompose H0. subst.
+   auto new timeout=100.
+ ].
 qed.
 
 theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
-- 
2.39.2