Natural-number congruences

Two distinct residues a, b < p never differ by a multiple of p: if b ≤ p * m + a, so that the natural subtraction does not truncate, the difference p * m + a - b is not divisible by p. This is the arithmetic behind the uniqueness of the decomposition of an exponent as p • μ + ν with ν i < p. Likewise, since (p - 1) a ≡ -a modulo p, two residues a, b < p with p ∣ (p - 1) a + b are equal.

Main results

• Nat.not_dvd_mul_add_sub: for distinct a, b < p with b ≤ p * m + a, p does not divide p * m + a - b.
• Nat.eq_of_dvd_sub_one_mul_add: for residues a, b < p, p ∣ (p - 1) * a + b forces b = a.
• TauCeti.sq_sub_one_eq_four_mul_of_mod_four_eq_three: for q ≡ 3 (mod 4), factor q² - 1 with the factor 4 made explicit.

theorem Nat.not_dvd_mul_add_sub {p m a b : ℕ} (ha : a < p) (hb : b < p) (hab : a ≠ b) (hle : b ≤ p * m + a) : ¬p ∣ p * m + a - b

Two distinct residues modulo p do not differ by a multiple of p.

theorem Nat.eq_of_dvd_sub_one_mul_add {p a b : ℕ} (ha : a < p) (hb : b < p) (h : p ∣ (p - 1) * a + b) : b = a

Two residues a, b < p with p ∣ (p - 1) * a + b are equal, since (p - 1) * a ≡ -a modulo p.

theorem TauCeti.sq_sub_one_eq_four_mul_of_mod_four_eq_three {q : ℕ} (hq : q % 4 = 3) : q ^ 2 - 1 = 4 * (q - 1) * ((q + 1) / 4)

For q ≡ 3 (mod 4), factor q² - 1 with the factor 4 made explicit.