(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ex0/defs.ma".
+include "Basic-1/ex0/defs.ma".
-include "LambdaDelta-1/leq/defs.ma".
+include "Basic-1/leq/defs.ma".
-include "LambdaDelta-1/aplus/props.ma".
+include "Basic-1/aplus/props.ma".
theorem aplus_gz_le:
\forall (k: nat).(\forall (h: nat).(\forall (n: nat).((le h k) \to (eq 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 H_y))))))) h)))) k).
+(* COMMENTS
+Initial nodes: 683
+END *)
theorem aplus_gz_ge:
\forall (n: nat).(\forall (k: nat).(\forall (h: nat).((le k h) \to (eq A
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)).
+(* COMMENTS
+Initial nodes: 524
+END *)
theorem next_plus_gz:
\forall (n: nat).(\forall (h: nat).(eq nat (next_plus gz n h) (plus h n)))
(next_plus gz n n0) (plus n0 n))) (refl_equal nat n) (\lambda (n0:
nat).(\lambda (H: (eq nat (next_plus gz n n0) (plus n0 n))).(f_equal nat nat
S (next_plus gz n n0) (plus n0 n) H))) h)).
+(* COMMENTS
+Initial nodes: 77
+END *)
theorem leqz_leq:
\forall (a1: A).(\forall (a2: A).((leq gz a1 a2) \to (leqz a1 a2)))
A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4:
A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4
a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
+(* COMMENTS
+Initial nodes: 1375
+END *)
theorem leq_leqz:
\forall (a1: A).(\forall (a2: A).((leqz a1 a2) \to (leq gz a1 a2)))
A).(\lambda (a3: A).(\lambda (_: (leqz a0 a3)).(\lambda (H1: (leq gz a0
a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leqz a4 a5)).(\lambda
(H3: (leq gz a4 a5)).(leq_head gz a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
+(* COMMENTS
+Initial nodes: 717
+END *)