n : ℕ
h₁ : 1 < n
h₂ : ¬Nat.Prime n
⊢ n ∣ 1 ^ (n - 1) - 1
n : ℕ
h₁ : 1 < n
h₂ : ¬Nat.Prime n
⊢ FermatPsp n 1
refine' ⟨show n ∣ 1 ^ (n - 1) - 1 from _, h₂, h₁⟩
no goals
n : ℕ
h₁ : 1 < n
h₂ : ¬Nat.Prime n
⊢ n ∣ 1 ^ (n - 1) - 1
exact show 0 = 1 ^ (n - 1) - 1 by norm_num ▸ dvd_zero n
no goals
n : ℕ
h₁ : 1 < n
h₂ : ¬Nat.Prime n
⊢ 0 = 1 ^ (n - 1) - 1
norm_num