Event: Start with the initial nqthm theory.

Theorem: plus-difference-shit ((z < y) ∧ (b ≤ a)) → (((y + a) − (z + b)) = ((y − z) + (a − b)))

Theorem: times-lessp (b ≮ a) → (((x ∗ b) < (x ∗ a)) = f)

Theorem: difference-lessp (a ≮ b) → ((b − a) = 0)

Theorem: lessp-plus ((a ≮ b) ∧ (c ≮ d)) → (((a + c) < (b + d)) = f)

Theorem: times-difference-dist (x ∗ (y − z)) = ((x ∗ y) − (x ∗ z))

Index

difference-lessp, 1 lessp-plus, 1 plus-difference-shit, 1 times-difference-dist, 1 times-lessp, 1