(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/ex0/defs.ma".
+include "LambdaDelta-1/leq/defs.ma".
-include "ex0/defs.ma".
-
-include "leq/defs.ma".
-
-include "aplus/props.ma".
+include "LambdaDelta-1/aplus/props.ma".
theorem aplus_gz_le:
\forall (k: nat).(\forall (h: nat).(\forall (n: nat).((le h k) \to (eq A
nat).(\lambda (_: ((\forall (n0: nat).((le n (S k0)) \to (eq A (asucc gz
(aplus gz (ASort n n0) k0)) (ASort O (plus (match n with [O \Rightarrow (S
k0) | (S l) \Rightarrow (minus k0 l)]) n0))))))).(\lambda (n0: nat).(\lambda
-(H0: (le (S n) (S k0))).(ex2_ind nat (\lambda (n1: nat).(eq nat (S k0) (S
-n1))) (\lambda (n1: nat).(le n n1)) (eq A (asucc gz (aplus gz (ASort (S n)
-n0) k0)) (ASort O (plus (minus k0 n) n0))) (\lambda (x: nat).(\lambda (H1:
-(eq nat (S k0) (S x))).(\lambda (H2: (le n x)).(let H3 \def (f_equal nat nat
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with [O
-\Rightarrow k0 | (S n1) \Rightarrow n1])) (S k0) (S x) H1) in (let H4 \def
-(eq_ind_r nat x (\lambda (n1: nat).(le n n1)) H2 k0 H3) in (eq_ind A (aplus
-gz (ASort n n0) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n)
-n0) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a:
+(H0: (le (S n) (S k0))).(let H_y \def (le_S_n n k0 H0) in (eq_ind A (aplus gz
+(ASort n n0) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n) n0)
+k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a:
A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0)
k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S
-n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H4))))))) (le_gen_S n (S
-k0) H0)))))) h)))) k).
+n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
theorem aplus_gz_ge:
\forall (n: nat).(\forall (k: nat).(\forall (h: nat).((le k h) \to (eq A
I (S x) H0) in (False_ind (eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O
n)) H2))))) (le_gen_S k0 O H))) (\lambda (n0: nat).(\lambda (_: (((le (S k0)
n0) \to (eq A (asucc gz (aplus gz (ASort n0 n) k0)) (ASort (minus n0 (S k0))
-n))))).(\lambda (H0: (le (S k0) (S n0))).(ex2_ind nat (\lambda (n1: nat).(eq
-nat (S n0) (S n1))) (\lambda (n1: nat).(le k0 n1)) (eq A (asucc gz (aplus gz
-(ASort (S n0) n) k0)) (ASort (minus n0 k0) n)) (\lambda (x: nat).(\lambda
-(H1: (eq nat (S n0) (S x))).(\lambda (H2: (le k0 x)).(let H3 \def (f_equal
-nat nat (\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with
-[O \Rightarrow n0 | (S n1) \Rightarrow n1])) (S n0) (S x) H1) in (let H4 \def
-(eq_ind_r nat x (\lambda (n1: nat).(le k0 n1)) H2 n0 H3) in (eq_ind A (aplus
-gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n0)
-n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) k0) (\lambda (a:
-A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus gz (ASort n0 n)
-k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc gz k0 (ASort (S
-n0) n))) (ASort (minus n0 k0) n) (IH n0 H4))))))) (le_gen_S k0 (S n0) H0)))))
-h)))) k)).
+n))))).(\lambda (H0: (le (S k0) (S n0))).(let H_y \def (le_S_n k0 n0 H0) in
+(eq_ind A (aplus gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus
+gz (ASort (S n0) n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n))
+k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus
+gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc
+gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
theorem next_plus_gz:
\forall (n: nat).(\forall (h: nat).(eq nat (next_plus gz n h) (plus h n)))