##
## redirect natural_specific.gh
##
param (PROP /peano_new/prop.ghi () "")
param (PREDICATE /peano_new/predicate_eq.ghi (PROP) "")
param (NATURALS /peano_new/arithmetic/common/naturals.ghi (PROP PREDICATE) "")
param (SET_MIN /peano_new/set_min.ghi (PROP PREDICATE) "")
# This file contains theorems that are involve natural numbers. These theorems are safe
# to apply to other categories of numbers since the natural number requirements are included
# in the theorem. The theorems in import.ghi are what allow these theorems to be exported
# into other contexts, so those theorems should be proved for each context in which these are
# used.
tvar (wff ph ps ch th ta)
tvar (nat A B C D)
var (nat v w x y z)
term (set (N))
stmt (0le () () (-> (e. A (N)) (<= (0) A)))
stmt (addge01t () () (-> (/\ (e. A (N)) (e. B (N))) (<= A (+ A B))))
stmt (addge02t () () (-> (/\ (e. A (N)) (e. B (N))) (<= A (+ B A))))
stmt (provele () () (-> (/\ (e. A (N)) (/\ (e. B (N)) (e. C (N)))) (-> (= (+ A B) C) (<= A C))))
stmt (lefoo3 () () (-> (/\ (e. A (N)) (e. B (N))) (<-> (<= A B) (\/ (= A B) (<= (+ A (1)) B)))))
## 0 is a Natural Number
stmt (0nat () () (e. (0) (N)))
## 1 is a Natural Number
stmt (1nat () () (e. (1) (N)))
stmt (addClosure () () (-> (/\ (e. A (N)) (e. B (N))) (e. (+ A B) (N))))
stmt (mulClosure () () (-> (/\ (e. A (N)) (e. B (N))) (e. (* A B) (N))))