English
For every n, MinSqFacProp(n, minSqFac(n)) holds.
Русский
Для каждого n верно, что MinSqFacProp(n, minSqFac(n)) выполняется.
LaTeX
$$$MinSqFacProp(n, minSqFac(n))$$$
Lean4
theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n) :=
by
dsimp only [minSqFac]; split_ifs with d2 d4
· exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩
· rcases Nat.eq_zero_or_pos n with n0 | n0
· subst n0
cases d4 (by decide)
refine minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_
refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
rintro rfl
contradiction
· rcases Nat.eq_zero_or_pos n with n0 | n0
· subst n0
cases d2 (by decide)
refine minSqFacAux_has_prop _ n0 0 rfl ?_
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
rintro rfl
contradiction
