+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.
+