NLE is now derived fron NPlus rather than being a stand-alone relation

diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma
index 59c02653ef17d827cb897d817fbaef5dca6397bf..a9b33561db8d542265c989c5fd6898ff11aab35c 100644 (file)
--- 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 661e00ecd523046e1ebeef50e90492cf91ad458e..f61fadfeee5f2b42b24b73aeca5b037c1e6af0be 100644 (file)
--- 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 bd76c2754b61db4aa5b540735245ae49eea16331..b571dfc6b46f9e8ab9385bef2462baf354e1d286 100644 (file)
--- 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.