case h
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r
p r i : ℕ
hr : ¬p ∣ r
⊢ ↑(factorization (p * i + r)) p = 0
apply factorization_eq_zero_of_not_dvd
no goals
case h
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r
rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]