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