X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=dad1f938241812ef41928b983c6cb984f5ae5f2d;hb=89ea663d91904f483f8248cfaeaed5eda8715da2;hp=83322f4d8de57107b0eeb097bb7cd96d3cd83d86;hpb=9a6cf8c3b53fe33515acd1aef8e7c7a10d71ae71;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 83322f4d8..dad1f9382 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -96,6 +96,20 @@ qed.
 lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
 /2 width=1 by plus_minus/ qed-.
 
+lemma idempotent_max: ∀n:nat. n = (n ∨ n).
+#n normalize >le_to_leb_true //
+qed.
+
+lemma associative_max: associative … max.
+#x #y #z normalize
+@(leb_elim x y) normalize #Hxy
+@(leb_elim y z) normalize #Hyz //
+[1,2: >le_to_leb_true /2 width=3 by transitive_le/
+| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/
+  >not_le_to_leb_false //
+]
+qed.
+
 (* Properties ***************************************************************)
 
 lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).