## ## Naturals ../naturals/inequality_min.gh ## Integers ../integers/inequality_min.gh ## Rationals ../rationals/NaN_construction/division_NaN.gh ## Rationals2 ../rationals/division_min.gh ## param (PROP prop.ghi () "") param (PREDICATE_EQ predicate_eq.ghi (PROP) "") param (ADD_MULTIPLY_MIN add_multiply_min.ghi (PROP PREDICATE_EQ) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) var (nat x) term (wff (<= A B)) ## Reflexive Property stmt (leid () () (<= A A)) ## Same upper and lower bound implies equality ## Trichotomy law (may be a poor choice of name) ## left('Simplify', '=') stmt (lesym () () (<-> (= A B) (/\ (<= A B) (<= B A)))) ## Total Relationship ## Less than or equal is a total relationship stmt (letot () () (\/ (<= A B) (<= B A))) ## Transitive Property ## right('Simplify', '≤ ≤') stmt (letr () () (-> (/\ (<= A B) (<= B C)) (<= A C))) ## Inequality Multiplication stmt (lemul1 () () (-> (/\ (<= A B) (<= (0) C)) (<= (* A C) (* B C)))) ## 0 is less than or equal to 1 stmt (0le1 () () (<= (0) (1))) ## Inequality Equivalence stmt (leeq1 () () (-> (= A B) (<-> (<= A C) (<= B C)))) ## Inequality Equivalence stmt (leeq2 () () (-> (= A B) (<-> (<= C A) (<= C B)))) ## Less Than or Equal from Nonnegative Difference stmt (exle ((A x)(B x)) () (<-> (<= A B) (E. x (/\ (<= (0) x) (= (+ A x) B)))))