-- Does there exist an odd perfect number? -- (A number n is perfect if it equals the sum of its proper divisors.) theorem no_odd_perfect : ∀ n : ℕ, Odd n → ¬(∑ d ∈ Nat.divisors n {n}, d = n) :=