List of theorems

List of theorems in general/First-order_linear_order_defined_via_nonstrict_inequality.gh:

(≤ a a)
(→ (= b0 b1) (↔ (≤ a b0) (≤ a b1)))
(→ (= a0 a1) (↔ (≤ a0 b) (≤ a1 b)))
(= a0 a1) , (= b0 b1)(↔ (≤ a0 b0) (≤ a1 b1))
(= a0 a1)(↔ (≤ a0 b) (≤ a1 b))
(= b0 b1)(↔ (≤ a b0) (≤ a b1))
(→ (= a b) (≤ a b))
(↔ (< a b) (∧ (≤ a b) (¬ (= a b))))
(↔ (> b a) (< a b))
(↔ (≥ b a) (≤ a b))
(↔ (≤ a b) (∧ (∨ (≤ a b) (= a b)) (∨ (¬ (= a b)) (= a b))))
(↔ (≤ a b) (∨ (< a b) (= a b)))
(→ (∧ (= a0 a1) (= b0 b1)) (↔ (< a0 b0) (< a1 b1)))
(→ (= b0 b1) (↔ (< a b0) (< a b1)))
(→ (= a0 a1) (↔ (< a0 b) (< a1 b)))
(= a0 a1) , (= b0 b1)(↔ (< a0 b0) (< a1 b1))
(= b0 b1)(↔ (< a b0) (< a b1))
(= a0 a1)(↔ (< a0 b) (< a1 b))
(→ (∧ (≤ a b) (< b c)) (≤ a c))
(→ (∧ (≤ a b) (< b c)) (¬ (= a c)))
(→ (∧ (≤ a b) (< b c)) (< a c))
(→ (< a b) (≤ a b))
(→ (∧ (< a b) (< b c)) (< a c))
(∨ (∨ (< a b) (= a b)) (< b a))
(→ (< a b) (¬ (= a b)))
(→ (< a b) (¬ (> a b)))
(→ (= a b) (¬ (< a b)))
(¬ (< a a))