update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_max.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
index 4e1e88280e08d62ae95c6fa88dc70884c99a0371..cb902736e1de5bbc7c1c02d33a2a79d4fadc4fad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/zero_0.ma".
 include "ground/arith/nat_succ_tri.ma".
 
 (* MAXIMUM FOR NON-NEGATIVE INTEGERS ****************************************)
@@ -40,7 +39,7 @@ qed.
 (*** max_SS *)
 lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 #n1 #n2
-@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion  gets in the way *)
+@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)
 <ntri_f_tri //
 qed.
 
@@ -52,20 +51,27 @@ lemma nmax_idem (n): n = (n ∨ n).
 
 (*** commutative_max *)
 lemma nmax_comm: commutative … nmax.
-#m #n @(nat_ind_succ_2 … m n) -m -n //
+#m #n @(nat_ind_2_succ … m n) -m -n //
 qed-.
 
 (*** associative_max *)
 lemma nmax_assoc: associative … nmax.
-#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 //
+#n1 #n2 @(nat_ind_2_succ … n1 n2) -n1 -n2 //
 #n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 //
 qed.
 
+lemma nmax_max_comm_23 (o:nat) (m) (n): (o ∨ m ∨ n) = (o ∨ n ∨ m).
+#o #m #n >nmax_assoc >nmax_assoc <nmax_comm in ⊢ (??(??%)?); //
+qed.
+
 (* Basic inversions *********************************************************)
 
-(*** max_inv_O3 *)
-lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
-#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 /2 width=1 by conj/
+lemma eq_inv_zero_nmax (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
+#n1 #n2 @(nat_ind_2_succ … n1 n2) -n1 -n2 /2 width=1 by conj/
 #n1 #n2 #_ <nmax_succ_bi #H
-elim (eq_inv_nzero_succ … H)
+elim (eq_inv_zero_nsucc … H)
 qed-.
+
+(*** max_inv_O3 *)
+lemma eq_inv_nmax_zero (n1) (n2): (n1 ∨ n2) = 𝟎 → ∧∧ 𝟎 = n1 & 𝟎 = n2.
+/2 width=1 by eq_inv_zero_nmax/ qed-.