Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Base-1 / ext / arith.ma

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 95d322b55a282bc2d8f40dd4f297e71fe3f6c64a..8be48633f5e4995871da5fa102e540cf5a763dd3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
-
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 theorem nat_dec:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
@@ -63,16 +61,21 @@ 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)))
+\def
+ \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
 
 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 
@@ -82,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 
@@ -93,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 
@@ -208,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))))))).
@@ -303,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 
@@ -353,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)))))
@@ -384,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)) 
@@ -439,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) 
@@ -451,10 +453,10 @@ h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
 (plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat 
 (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) (lt_le_S (plus (plus d2 h2) h1) (S (plus n h1)) 
-(le_lt_n_Sm (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) (minus_plus h2 (plus d2 h1))))))).
+(plus d2 h2) h1) (plus n h1) (le_n_S (plus (plus d2 h2) h1) (plus n 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:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
@@ -501,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: 
@@ -545,13 +548,11 @@ nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O
 \def (IH O O) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: 
 nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq 
 nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0)) 
-in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n 
-z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq 
-nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) 
-H1)))))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall 
-(y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) 
-(plus (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) 
-y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2: 
+in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (eq_add_S (plus z0 y1) (plus z0 y2) 
+H1))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall (y2: 
+nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) (plus 
+(match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) y2)) 
+\to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2: 
 nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda 
 (H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O 
 x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: 
@@ -599,8 +600,8 @@ theorem le_S_minus:
  \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus 
 d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1 
 \def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h) 
-(le_plus_minus_sym h n (le_trans_plus_r d h n H))) in (le_S d (minus n h) 
-(le_minus d n h H))))))).
+(le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S 
+d (minus n h) (le_minus d n h H))))))).
 
 theorem lt_x_pred_y:
  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))