X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Farith.ma;h=39d28c959182d17c31fa4a851751928c3fc12b8d;hb=b5db76fe31ab35bae0257cb6684c511bcc531e45;hp=418a176d5024ab7e8190c2c3220d7e45c1b3d0b2;hpb=35653f628dc3a3e665fee01acc19c660c9d555e3;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
index 418a176d5..39d28c959 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
@@ -17,7 +17,7 @@ include "Ground_2/star.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
-(* equations ****************************************************************)
+(* Equations ****************************************************************)
 
 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 /2 by plus_minus/ qed.
@@ -69,4 +69,8 @@ qed-.
 (*
 lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
 /3 width=2/
+
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (lt_or_ge m n) /2 width=1/ /3 width=2/
+qed-.
 *)