theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n

theorem card_units (p : ℕ) [Fact (Nat.Prime p)] : Fintype.card (ZMod p)ˣ = p - 1

theorem Int.NatAbs_natCast_ori (n : ℕ) : (↑n).natAbs = n

theorem val_natCast (n a : ℕ) : (↑a).val = a % n

theorem eq_iff_modEq_nat_fermat (n : ℕ) {a b : ℕ} : ↑a = ↑b ↔ a ≡ b [MOD n]

theorem dvd_choose (p a b : ℕ) (hp : Nat.Prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) : p ∣ b.choose a

theorem nat_cast_eq_zero_iff_dvd {p n : ℕ} [hp : Fact (Nat.Prime p)] : ↑n = 0 ↔ p ∣ n

theorem fermat2_pre {a p : ℕ} (hp : Nat.Prime p) : (a + 1) ^ p ≡ a ^ p + 1 [MOD p]

theorem fermat_binomial_theorem (p : ℕ) (hp : Nat.Prime p) (n : ℕ) : (n + 1) ^ p ≡ n + 1 [MOD p]

theorem Nat.not_dvd_one {a : ℕ} (h : a ≠ 1) : ¬a ∣ 1

theorem Nat.coprime_not_dvd {a b : ℕ} (h : a.Coprime b) (hne : a ≠ 1) : ¬a ∣ b

theorem fermat_via_binomial (p n : ℕ) (hp : Nat.Prime p) (hcoprime : (n + 1).Coprime p) : (n + 1) ^ (p - 1) ≡ 1 [MOD p]

theorem katabami_theorem_fermat2 {n p : ℕ} (hp : Nat.Prime p) (hn : n.Coprime p) (hn_pos : 0 < n) : n ^ (p - 1) ≡ 1 [MOD p]

theorem katabami_theorem_fermat3 (p : ℕ) [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) : a ^ (p - 1) = 1