latte-nats.ord
The oredering relation for natural numbers.
<=
(<= [m nat] [n nat])
(exists [k nat] (= (+ m k) n))
Definition: The lower-or-equal order for natural numbers.
le-antisym
(le-antisym [m nat] [n nat])
(==> (<= m n) (<= n m) (= m n))
Theorem:
le-refl
(le-refl [n nat])
(<= n n)
Theorem:
le-trans
(le-trans [m nat] [n nat] [p nat])
(==> (<= m n) (<= n p) (<= m p))
Theorem:
lt-asym
(lt-asym [n nat] [m nat])
(==> (< n m) (not (< m n)))
Theorem:
lt-le
(lt-le [m nat] [n nat])
(==> (< m n) (<= m n))
Theorem:
lt-trans
(lt-trans [n nat] [m nat] [p nat])
(==> (< n m) (< m p) (< n p))
Theorem:
lt-trans-weak
(lt-trans-weak [n nat] [m nat] [p nat])
(==> (<= n m) (< m p) (< n p))
Theorem:
lt-trans-weak-alt
(lt-trans-weak-alt [n nat] [m nat] [p nat])
(==> (< n m) (<= m p) (< n p))
Theorem: An alternative to lt-trans-weak.
plus-le
(plus-le [m nat] [n nat] [p nat])
(==> (<= (+ m p) (+ n p)) (<= m n))
Theorem:
plus-le-conv
(plus-le-conv [m nat] [n nat] [p nat])
(==> (<= m n) (<= (+ m p) (+ n p)))
Theorem: The converse of plus-le.