proposed lemmas for mathlib

Stream: general

[Scott Morrison]

I'd like to add

lemma min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬ prime n) : min_fac n ≤ n / min_fac n := ...

to mathlib.

I have an (almost-surely-pessimal) proof, so I'm not asking about that for now, just asking about suitability for mathlib.

[Scott Morrison]

One could make an iff version too.

[Johan Commelin]

Seems legit

[Reid Barton]

What's the iff version?

[Reid Barton]

I hope your proof begins apply min_fac_le_of_dvd,

[Johan Commelin]

I guess : ¬ prime n \iff min_fac n ≤ n / min_fac n

[Reid Barton]

Oh that makes sense. I was imaging something like "p is the minimum factor of n if and only if ..." and got stuck.