we added a definition and a couple of lemmas

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index f4d78234f7ef1a4ea3282d6f97dd343ad74354b6..a20311ced3047dd62ab4efb4c4f106a912a2ad7c 100644 (file)
--- 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 a1bae198b707723b66f5ba16db61ac1cac58deab..a82f314f698e9dc23fb479c56848c83b586d2654 100644 (file)
--- 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 d17dcca7ec4fc727e5503e75f21cc0be8d3e0ca8..cae3766b1d008bf2b41c9ecb50360ea9ce00ec44 100644 (file)
--- 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.