(* 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
(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)))
\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
(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
\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
\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))))))).
\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
\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)))))
\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))
\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)
(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:
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: