n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat (minFac n) k
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat (minFac n) k
rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2
no goals
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat (minFac n) k
exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩