case intro.intro
n b : ℕ
h₁ : 1 ≤ b
hp : ProbablePrime n b
left✝ : ¬Nat.Prime n
hn₂ : 1 < n
⊢ Nat.coprime n b
n b : ℕ
h : FermatPsp n b
h₁ : 1 ≤ b
⊢ Nat.coprime n b
rcases h with ⟨hp, _, hn₂⟩
no goals
case intro.intro
n b : ℕ
h₁ : 1 ≤ b
hp : ProbablePrime n b
left✝ : ¬Nat.Prime n
hn₂ : 1 < n
⊢ Nat.coprime n b
exact coprime_of_probablePrime hp (by linarith) h₁
no goals
n b : ℕ
h₁ : 1 ≤ b
hp : ProbablePrime n b
left✝ : ¬Nat.Prime n
hn₂ : 1 < n
⊢ 1 ≤ n
linarith