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

The $$\sim$$ relation is reflexive.

Proof available

THEOREM

The $$\sim$$ relation is symmetric.

Proof available

THEOREM

The $$\sim$$ relation is transitive.

Proof available

THEOREM

Consecutive integers are coprime.

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


Proof available

THEOREM

Integer addition is commutative.

Proof available

THEOREM

Integer addition is associative.

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