latte-nats.ord

The oredering relation for natural numbers.

<

(< [n nat] [m nat])
(and (<= n m) (not (= n m)))

Definition: The strict variant of <=.

<=

(<= [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.