latte-integers.minus
The subtraction (and opposite) defined on ℤ.
-
(- [n int] [m int])(q/the (minus-unique n m))
Definition: Integer subtraction.
--
(-- [n int])(- zero n)
Definition: The opposite of an integer.
assoc-minus-minus
(assoc-minus-minus [n int] [m int] [p int])(= (- n (- m p)) (+ (- n m) p))
Theorem:
assoc-minus-minus-sym
(assoc-minus-minus-sym [n int] [m int] [p int])(= (+ (- n m) p) (- n (- m p)))
Theorem:
assoc-minus-plus
(assoc-minus-plus [n int] [m int] [p int])(= (- n (+ m p)) (- (- n m) p))
Theorem:
assoc-minus-plus-sym
(assoc-minus-plus-sym [n int] [m int] [p int])(= (- (- n m) p) (- n (+ m p)))
Theorem:
assoc-plus-minus
(assoc-plus-minus [n int] [m int] [p int])(= (+ n (- m p)) (- (+ n m) p))
Theorem:
assoc-plus-minus-sym
(assoc-plus-minus-sym [n int] [m int] [p int])(= (- (+ n m) p) (+ n (- m p)))
Theorem:
minus-cancel
(minus-cancel [n int])(= (- n n) zero)
Theorem:
minus-left-cancel
(minus-left-cancel [n int] [m int] [p int])(==> (= (- n m) (- n p)) (= m p))
Theorem:
minus-one
(minus-one [n int])(= (- n one) (pred n))
Theorem:
minus-opp
(minus-opp [n int] [m int])(= (- n m) (- (-- m) (-- n)))
Theorem: A property about negation of opposites.
minus-opp-cancel
(minus-opp-cancel [n int] [m int])(==> (= (-- n) (-- m)) (= n m))
Theorem: A cancellation law for subtraction of opposites.
minus-pos-neg
(minus-pos-neg [n int] [m int])(==> (positive (- n m)) (negative (- m n)))
Theorem:
minus-pos-neg-conv
(minus-pos-neg-conv [n int] [m int])(==> (negative (- m n)) (positive (- n m)))
Theorem:
minus-pos-neg-equiv
(minus-pos-neg-equiv [n int] [m int])(<=> (positive (- n m)) (negative (- m n)))
Theorem:
minus-pred
(minus-pred [n int] [m int])(= (- (pred n) m) (pred (- n m)))
Theorem:
minus-pred-succ
(minus-pred-succ [n int] [m int])(= (- n (pred m)) (succ (- n m)))
Theorem:
minus-pred-succ-sym
(minus-pred-succ-sym [n int] [m int])(= (succ (- n m)) (- n (pred m)))
Theorem:
minus-prop
(minus-prop [n int] [m int])(= (+ (- n m) m) n)
Theorem: The defining property of subtraction.
minus-prop-cons
(minus-prop-cons [n int] [m int])(= (- (+ n m) m) n)
Theorem: A consequence of minus-prop.
minus-right-cancel
(minus-right-cancel [n int] [m int] [p int])(==> (= (- n p) (- m p)) (= n m))
Theorem:
minus-succ
(minus-succ [n int] [m int])(= (- (succ n) m) (succ (- n m)))
Theorem:
minus-succ-pred
(minus-succ-pred [n int] [m int])(= (- n (succ m)) (pred (- n m)))
Theorem:
minus-succ-pred-sym
(minus-succ-pred-sym [n int] [m int])(= (pred (- n m)) (- n (succ m)))
Theorem:
minus-unique
(minus-unique [n int] [m int])(q/unique (lambda [p int] (= (+ p m) n)))
Theorem: The unicity property of subtraction.
minus-zero
(minus-zero [n int])(= (- n zero) n)
Theorem:
minus-zero-alt
(minus-zero-alt [m int] [n int])(==> (= (- m n) zero) (= m n))
Theorem:
minus-zero-alt-conv
(minus-zero-alt-conv [m int] [n int])(==> (= m n) (= (- m n) zero))
Theorem:
nat-split-opp
(nat-split-opp [n int])(or (elem n nat) (elem (-- n) nat))
Theorem: A variant of nat splitting.
opp-and-zero
(opp-and-zero [n int])(==> (and (elem n nat) (elem (-- n) nat)) (= n zero))
Theorem:
opp-eq
(opp-eq [m int] [n int])(==> (= (-- m) n) (= m (-- n)))
Theorem:
opp-nat-split
(opp-nat-split [n int])(==> (elem (-- n) nat) (or (= n zero) (negative n)))
Theorem:
opp-nat-split-conv
(opp-nat-split-conv [n int])(==> (or (= n zero) (negative n)) (elem (-- n) nat))
Theorem:
opp-nat-split-equiv
(opp-nat-split-equiv [n int])(<=> (elem (-- n) nat) (or (= n zero) (negative n)))
Theorem:
opp-neg-pos
(opp-neg-pos [n int])(==> (negative n) (positive (-- n)))
Theorem:
opp-neg-pos-conv
(opp-neg-pos-conv [n int])(==> (positive (-- n)) (negative n))
Theorem:
opp-neg-pos-equiv
(opp-neg-pos-equiv [n int])(<=> (negative n) (positive (-- n)))
Theorem:
opp-neg-split
(opp-neg-split [n int])(or (or (= n zero) (negative n)) (negative (-- n)))
Theorem: A split for integers using the opposite, using nat/negative.
opp-opp
(opp-opp [n int])(= (-- (-- n)) n)
Theorem:
opp-plus
(opp-plus [n int] [m int])(= (-- (+ n m)) (- (-- n) m))
Theorem:
opp-plus-opp
(opp-plus-opp [n int])(= (+ (-- n) n) zero)
Theorem:
opp-pos-neg
(opp-pos-neg [n int])(==> (positive n) (negative (-- n)))
Theorem:
opp-pos-neg-conv
(opp-pos-neg-conv [n int])(==> (negative (-- n)) (positive n))
Theorem:
opp-pos-neg-equiv
(opp-pos-neg-equiv [n int])(<=> (positive n) (negative (-- n)))
Theorem:
opp-pos-split
(opp-pos-split [n int])(or (or (= n zero) (positive n)) (positive (-- n)))
Theorem: A split for integers using the opposite, using nat/positive.
opp-pred-succ
(opp-pred-succ [n int])(= (-- (pred n)) (succ (-- n)))
Theorem:
opp-succ-pred
(opp-succ-pred [n int])(= (-- (succ n)) (pred (-- n)))
Theorem:
opp-zero
(opp-zero)(= (-- zero) zero)
Theorem:
plus-opp-minus
(plus-opp-minus [n int] [m int])(= (+ n (-- m)) (- n m))
Theorem:
plus-zero-minus
(plus-zero-minus [n int] [m int])(= (+ (- zero n) m) (- m n))
Theorem:
zero-opp-zero
(zero-opp-zero [n int])(==> (= n zero) (= (-- n) zero))
Theorem:
zero-opp-zero-conv
(zero-opp-zero-conv [n int])(==> (= (-- n) zero) (= n zero))
Theorem:
zero-opp-zero-equiv
(zero-opp-zero-equiv [n int])(<=> (= n zero) (= (-- n) zero))
Theorem: