Euclidian division

Christophe Raffalli Équipe de logique de Paris VII (URA 753)

May 12, 1999

Theorem 1.

∀p,d:IN (d ≠ 0 → ∃q,r:IN (r < d ∧ p = q.d + r))

Proof. Let us choose p, d two natural numbers with d ≠ 0. We prove the following by induction on p: ∃q,r:IN (r < d ∧ p = q.d + r). Let us choose a a strictly positive natural. We assume

∀b:IN (b < a → ∃q,r:IN (r < d ∧ b = q.d + r))

and we must prove ∃q,r:IN (r < d ∧ a = q.d + r). We distinguish two cases: a < d and d ≤ a. In the first case, we choose q = 0 and r = a. In the second case, we take a′ = a − d. Using the induction hypothesis on a′, we find two naturals q, r such that r < d and a′ = q.d + r. We choose S q and r as quotient and remaining for the division of a. We must prove a = S q.d + r which is immediate.