case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = abs ↑p

case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < ↑p
convert Int.emod_lt _ _
no goals
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = abs ↑p
simp
no goals
case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
exact_mod_cast hp_prime.1.ne_zero