List of theorems

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

(→ (= 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) (¬ (= 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) (¬ (= a b))))
(∨ (≤ a b) (≤ b a))
(≤ a a)
(→ (∧ (= 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))
(= a0 a1)(↔ (≤ a0 b) (≤ a1 b))
(= b0 b1)(↔ (≤ a b0) (≤ a b1))
(→ (= a b) (≤ a b))
(→ (< a b) (≤ a b))
(→ (∧ (≤ a b) (< b c)) (< a c))
(→ (∧ (≤ a b) (≤ b c)) (≤ a c))
(→ (< a b) (¬ (> a b)))
(→ (= a b) (¬ (< a b)))
(→ (∧ (< a b) (≤ b a)) (= a b))
(→ (∧ (≤ a b) (≤ b a)) (= a b))