# Integer

THEOREM

Define a relation $$\sim$$ such that:

$$\forall (a,b),(c,d) \in \mathbb{N}\times\mathbb{N}: (a,b)\sim(c,d) \Leftrightarrow a + d = b + c$$

Then $$\sim$$ is an equivalence relation.

Proof available

THEOREM

Consecutive integers are coprime.

GCD.semiring_gcd_class.coprime_add_one_right:
coprime ?a (?a + 1)


Proof available

THEOREM

The product of two negative numbers is positive.

Rings.linordered_ring_strict_class.mult_neg_neg:
?a < 0 $$\Longrightarrow$$ ?b < 0 $$\Longrightarrow$$ 0 < ?a * ?b


Proof unavailable

THEOREM    $$(a + c, b + c) \sim (a, b)$$

Proof available

THEOREM    $$(c + a, c + b) \sim (a, b)$$

Proof available

THEOREM    $$\forall x,y,z \in \mathbb{Z} : x \lt y \Rightarrow x + z \lt y + z$$

Proof available

THEOREM    $$\forall x,y,z \in \mathbb{Z} : x \lt y \Rightarrow z + x \lt z + y$$

Proof available