Composite_Number_has_Two_Divisors_Less_Than_It
Proveddivisorsproofwiki
A composite number greater than 1 can be expressed as the product of two positive integers strictly between 1 and n.
Preamble
import Mathlib.Data.Nat.Prime.Basic
Formal statement
theorem Composite_Number_has_Two_Divisors_Less_Than_It (n : ℕ) (hn : 1 < n) (hnp : ¬Nat.Prime n) : ∃ a b : ℕ, 1 < a ∧ a < n ∧ 1 < b ∧ b < n ∧ n = a * b := by sorry
Source