X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-1%2Fext%2Farith.ma;h=8be48633f5e4995871da5fa102e540cf5a763dd3;hb=3b2361afb73203749541ad07e94648da6057ae67;hp=0d0f2a5dfd98a69ce51bcd558054c3c24355eb53;hpb=0e9753cbccef485911e2c2de1b4cdcae592906b9;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
index 0d0f2a5df..8be48633f 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
@@ -61,10 +61,10 @@ theorem simpl_plus_r:
 (plus p n)) \to (eq nat m p))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat 
-(plus m n) (plus p n))).(plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda 
+(plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda 
 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: 
-nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n 
-p)) (plus m n) H) (plus n m) (plus_comm n m)))))).
+nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_sym n 
+p)) (plus m n) H) (plus n m) (plus_sym n m)))))).
 
 theorem minus_Sx_Sy:
  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
@@ -75,7 +75,7 @@ theorem minus_plus_r:
  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 \def
  \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: 
-nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_comm m n))).
+nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
 
 theorem plus_permute_2_in_3:
  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x 
@@ -85,9 +85,8 @@ y) z) (plus (plus x z) y))))
 (plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat 
 (plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind 
 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) 
-(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_reverse 
-x z y)) (plus y z) (plus_comm y z)) (plus (plus x y) z) (plus_assoc_reverse x 
-y z)))).
+(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z 
+y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
 
 theorem plus_permute_2_in_3_assoc:
  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n 
@@ -96,8 +95,8 @@ h) k) (plus n (plus k h)))))
  \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus 
 (plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r 
 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) 
-(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc n k h)) 
-(plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
+(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k 
+h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
 
 theorem plus_O:
  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
@@ -211,14 +210,14 @@ n))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat 
 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) 
-(plus (minus m n) n) (plus_comm (minus m n) n)))).
+(plus (minus m n) n) (plus_sym (minus m n) n)))).
 
 theorem le_minus_minus:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) 
 \to (le (minus y x) (minus z x))))))
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: 
-nat).(\lambda (H0: (le y z)).(plus_le_reg_l x (minus y x) (minus z x) 
+nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x) 
 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat 
 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z 
 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
@@ -306,17 +305,17 @@ theorem lt_x_plus_x_Sy:
 \def
  \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: 
 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) 
-(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_comm x (S y)))).
+(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
 
 theorem simpl_lt_plus_r:
  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
 p)) \to (lt n m))))
 \def
  \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus 
-n p) (plus m p))).(plus_lt_reg_l n m p (let H0 \def (eq_ind nat (plus n p) 
-(\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_comm n p)) in (let 
+n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p) 
+(\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let 
 H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 
-(plus p m) (plus_comm m p)) in H1)))))).
+(plus p m) (plus_sym m p)) in H1)))))).
 
 theorem minus_x_Sy:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
@@ -356,7 +355,7 @@ theorem lt_plus_minus_r:
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat 
 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x 
-y H) (plus (minus y (S x)) x) (plus_comm (minus y (S x)) x)))).
+y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
 
 theorem minus_x_SO:
  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
@@ -387,7 +386,7 @@ theorem lt_le_minus:
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S 
 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O)) 
-(plus_comm x (S O)))))).
+(plus_sym x (S O)))))).
 
 theorem lt_le_e:
  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
@@ -442,7 +441,7 @@ theorem lt_neq:
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq 
 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in 
-(lt_irrefl y H1))))).
+(lt_n_n y H1))))).
 
 theorem arith0:
  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) 
@@ -455,8 +454,8 @@ h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
 (plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat 
 (plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus 
 (plus d2 h2) h1) (plus n h1) (le_n_S (plus (plus d2 h2) h1) (plus n h1) 
-(plus_le_compat (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_comm 
-h2 d2)) (plus h2 (plus d2 h1)) (plus_assoc h2 d2 h1))) (plus d2 h1) 
+(le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2 
+d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1) 
 (minus_plus h2 (plus d2 h1))))))).
 
 theorem O_minus:
@@ -504,19 +503,20 @@ nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True
 nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus 
 y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: 
 nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S 
-z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (_: (le (S z0) (S 
+z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (H: (le (S z0) (S 
 x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) 
-(minus O (S z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda 
-(n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq 
-nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda 
-(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow 
-True | (S _) \Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0) 
-O) H4))))) (le_gen_S z0 O H0))))) (\lambda (y0: nat).(\lambda (_: (((le (S 
-z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0 
-(S z0))) \to (eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S 
-x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0) 
-(S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 
-x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
+(minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda 
+(n: nat).(eq nat O (S n))) (\lambda (n: nat).(le z0 n)) (eq nat (S x0) O) 
+(\lambda (x1: nat).(\lambda (H2: (eq nat O (S x1))).(\lambda (_: (le z0 
+x1)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return 
+(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) 
+I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0)))))) 
+(\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to 
+((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0) 
+y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S 
+y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S 
+z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) 
+H1))))))) y)))) x)))) z).
 
 theorem plus_plus:
  \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: