latte-integers.ord
The natural ordering on integers.
<=
(<= [n int] [m int])(elem (- m n) nat)
Definition: The lower-or-equal order for integers.
>=
(>= [n int] [m int])(<= m n)
Definition: The greater-or-equal order for integers.
le-antisym
(le-antisym [n int] [m int])(==> (<= n m) (<= m n) (= n m))
Theorem:
le-lt-split
(le-lt-split [m int] [n int])(==> (<= m n) (or (= m n) (< m n)))
Theorem:
le-refl
(le-refl [n int])(<= n n)
Theorem:
le-trans
(le-trans [n int] [m int] [p int])(==> (<= n m) (<= m p) (<= n p))
Theorem:
lt-asym
(lt-asym [n int] [m int])(==> (< n m) (not (< m n)))
Theorem:
lt-le
(lt-le [m int] [n int])(==> (< m n) (<= m n))
Theorem:
lt-opp-conv
(lt-opp-conv [n int] [m int])(==> (< (-- m) (-- n)) (< n m))
Theorem: The converse of lt-opp.
lt-opp-equiv
(lt-opp-equiv [n int] [m int])lt-pred
(lt-pred [m int])(< (pred m) m)
Theorem:
lt-pred-cong
(lt-pred-cong [m int] [n int])(==> (< m n) (< (pred m) (pred n)))
Theorem:
lt-pred-cong-conv
(lt-pred-cong-conv [m int] [n int])(==> (< (pred m) (pred n)) (< m n))
Theorem:
lt-succ
(lt-succ [n int])(< n (succ n))
Theorem: Strict ordering of successors.
lt-succ-cong
(lt-succ-cong [m int] [n int])(==> (< m n) (< (succ m) (succ n)))
Theorem:
lt-succ-cong-conv
(lt-succ-cong-conv [m int] [n int])(==> (< (succ m) (succ n)) (< m n))
Theorem:
lt-succ-weak
(lt-succ-weak [m int] [n int])(==> (< m (succ n)) (<= m n))
Theorem:
lt-trans
(lt-trans [n int] [m int] [p int])(==> (< n m) (< m p) (< n p))
Theorem:
lt-trans-weak
(lt-trans-weak [n int] [m int] [p int])(==> (<= n m) (< m p) (< n p))
Theorem:
lt-trans-weak-alt
(lt-trans-weak-alt [n int] [m int] [p int])(==> (< n m) (<= m p) (< n p))
Theorem: An alternative to lt-trans-weak.
lt-zero-opp
(lt-zero-opp [n int])(==> (< n zero) (> (-- n) zero))
Theorem:
lt-zero-opp-conv
(lt-zero-opp-conv [n int])(==> (> (-- n) zero) (< n zero))
Theorem:
lt-zero-opp-equiv
(lt-zero-opp-equiv [n int])(<=> (< n zero) (> (-- n) zero))
Theorem:
minus-lt
(minus-lt [m int] [n int] [p int])(==> (< (- m p) (- n p)) (< m n))
Theorem:
minus-lt-conv
(minus-lt-conv [m int] [n int] [p int])(==> (< m n) (< (- m p) (- n p)))
Theorem:
nat-ge-zero
(nat-ge-zero [n int])(==> (elem n nat) (>= n zero))
Theorem:
neg-lt-zero
(neg-lt-zero [n int])(==> (negative n) (< n zero))
Theorem:
neg-lt-zero-conv
(neg-lt-zero-conv [n int])(==> (< n zero) (negative n))
Theorem:
neg-lt-zero-equiv
(neg-lt-zero-equiv [n int])(<=> (negative n) (< n zero))
Theorem:
ord-int-split
(ord-int-split [n int])(or (or (= n zero) (> n zero)) (< n zero))
Theorem: Splitting an integer according to its (strict) ordering.
plus-le
(plus-le [n int] [m int] [p int])(==> (<= (+ n p) (+ m p)) (<= n m))
Theorem:
plus-le-cong
(plus-le-cong [m1 int] [m2 int] [n1 int] [n2 int])(==> (<= m1 n1) (<= m2 n2) (<= (+ m1 m2) (+ n1 n2)))
Theorem:
plus-le-conv
(plus-le-conv [n int] [m int] [p int])(==> (<= n m) (<= (+ n p) (+ m p)))
Theorem: The converse of plus-le.
plus-le-equiv
(plus-le-equiv [n int] [m int] [p int])(<=> (<= (+ n p) (+ m p)) (<= n m))
Theorem:
plus-lt
(plus-lt [n int] [m int] [p int])(==> (< (+ n p) (+ m p)) (< n m))
Theorem:
plus-lt-conv
(plus-lt-conv [n int] [m int] [p int])(==> (< n m) (< (+ n p) (+ m p)))
Theorem:
plus-lt-equiv
(plus-lt-equiv [n int] [m int] [p int])(<=> (< (+ n p) (+ m p)) (< n m))
Theorem:
pos-ge-one
(pos-ge-one [n int])(==> (positive n) (>= n one))
Theorem:
pos-gt-zero
(pos-gt-zero [n int])(==> (positive n) (> n zero))
Theorem:
pos-gt-zero-conv
(pos-gt-zero-conv [n int])(==> (> n zero) (positive n))
Theorem:
pos-gt-zero-equiv
(pos-gt-zero-equiv [n int])(<=> (positive n) (> n zero))
Theorem:
pos-one-split
(pos-one-split [n int])(==> (positive n) (or (= n one) (> n one)))
Theorem: A split princple for positive numbers wrt. int/one.