From aacce10080ef24f9851d760294c3e5d8233440cc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 6 Dec 2011 19:14:11 +0000
Subject: [PATCH] we added a definition and a couple of lemmas

---
 matita/matita/lib/arithmetics/nat.ma  |  5 +++++
 matita/matita/lib/basics/relations.ma |  5 +++++
 matita/matita/lib/basics/star.ma      | 14 ++++++++++++++
 3 files changed, 24 insertions(+)

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index f4d78234f..a20311ced 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -948,6 +948,11 @@ theorem monotonic_le_minus_r:
 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
 qed.
 
+theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
+#p #q #n #H1 #H2
+@lt_plus_to_minus_r <plus_minus_m_m //
+qed.
+
 theorem eq_minus_O: ∀n,m:nat.
   n ≤ m → n-m = O.
 #n #m #lenm @(le_n_O_elim (n-m)) /2/
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index a1bae198b..a82f314f6 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,6 +11,11 @@
 
 include "basics/logic.ma".
 
+(********** preducates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
 (********** relations **********)
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index d17dcca7e..cae3766b1 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -139,3 +139,17 @@ lemma WF_antimonotonic: ∀A,R,S. subR A R S →
 #H #Hind % #c #Rcb @Hind @subRS //
 qed.
 
+(* added from lambda_delta *)
+
+lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
+                R a1 a → TC … R a a2 → TC … R a1 a2.
+/3 width=3/ qed.
+
+lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
+/2 width=1/ qed.
+
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
+                   P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
+                   ∀a2. TC … R a1 a2 → P a2.
+#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
+qed.
-- 
2.39.2