confluence of parallel substitution (tps) started ...

[helm.git] / matita / matita / lib / lambda-delta / ground.ma

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 92a3f8167e54071e8283ff9f5ba0f557320c3c30..e09e7d47afbfa7e783852be619044dc8bd421a42 100644 (file)
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/nat.ma".
+include "lambda-delta/xoa_props.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
@@ -42,6 +43,14 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 #m #n elim (decidable_lt m n) /3/
 qed.
 
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m elim m -m
+[ * /2/
+| #m #IHm * [ /2/ ]
+  #n elim (IHm n) -IHm #H 
+  [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *)
+  qed. 
+
 lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
 #m #n * -n /3/
 qed.