X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_max.ma;h=4e1e88280e08d62ae95c6fa88dc70884c99a0371;hp=0032637b1d75bae73cb1322a59898b75969c9988;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hpb=68e028d053806177e218ee1a5f8778d3011bef83

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
index 0032637b1..4e1e88280 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -25,7 +25,7 @@ interpretation
   "maximum (non-negative integers)"
   'or m n = (nmax m n).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** max_O1 *)
 lemma nmax_zero_sn (n2): n2 = (𝟎 ∨ n2).
@@ -44,7 +44,7 @@ lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 <ntri_f_tri //
 qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 (*** idempotent_max *)
 lemma nmax_idem (n): n = (n ∨ n).
@@ -52,22 +52,20 @@ lemma nmax_idem (n): n = (n ∨ n).
 
 (*** commutative_max *)
 lemma nmax_comm: commutative … nmax.
-#m #n @(nat_ind_2 … m n) -m -n //
+#m #n @(nat_ind_succ_2 … m n) -m -n //
 qed-.
 
 (*** associative_max *)
 lemma nmax_assoc: associative … nmax.
-#n1 elim n1 -n1 //
-#n1 #IH #n2 elim n2 -n2 //
-#n2 #_ #n3 elim n3 -n3 //
-qed-.
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 //
+#n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 //
+qed.
 
 (* Basic inversions *********************************************************)
 
 (*** max_inv_O3 *)
 lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
-#n1 elim n1 -n1 [ /2 width=1 by conj/ ]
-#n1 #_ #n2 elim n2 -n2 [ /2 width=1 by conj/ ]
-#n2 #_ <nmax_succ_bi #H
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 /2 width=1 by conj/
+#n1 #n2 #_ <nmax_succ_bi #H
 elim (eq_inv_nzero_succ … H)
 qed-.