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