Composite_Number_has_Prime_Factor_not_Greater_Than_its_Square_Root

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Prime.Basic

theorem Composite_Number_has_Prime_Factor_not_Greater_Than_its_Square_Root (n : ℕ) (hn : 2 ≤ n) (hnp : ¬ Nat.Prime n) : ∃ p, Nat.Prime p ∧ p ∣ n ∧ p * p ≤ n := by sorry