LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Cancellation for multiplication by a nonzero factor

Statement

For all $m, n, k \in N$ with $k \neq 0$ : if $m \cdot k = n \cdot k$ then $m = n$ .

Facts & Assumptions

Given: multiplication defined by $m \cdot 0 = 0$ and $m \cdot σ (j) = m \cdot j + m$ ; the order $m \leq n ⟺ \exists j (m + j = n)$ , with $m < n$ meaning $m \leq n$ and $m \neq n$ .

[L1]

Trichotomy: for all $m, n \in N$ exactly one of $m < n$ , $m = n$ , $m > n$ holds (Trichotomy of the order on $N$ ).

[L2]

Strict monotonicity: if $k \neq 0$ and $m < n$ then $m \cdot k < n \cdot k$ (Order is compatible with multiplication).

Proof

technique · contradiction

1.1assume-contra

Suppose $m \cdot k = n \cdot k$ with $k \neq 0$ but $m \neq n$ .

2.1step 1.1L1

By trichotomy [L1], $m \neq n$ forces $m < n$ or $n < m$ .

3.1step 2.1L2

If $m < n$ then $m \cdot k < n \cdot k$ by [L2] (since $k \neq 0$ ); if $n < m$ then $n \cdot k < m \cdot k$ by [L2]; either way $m \cdot k \neq n \cdot k$ .

4.1step 1.1step 3.1discharge-contradiction∎

This contradicts $m \cdot k = n \cdot k$ , so the assumption $m \neq n$ is impossible and $m = n$ .

Cancellation for multiplication by a nonzero factor

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources