mathlib

b9798dc7 - feat(data/nat): a lemma about min_fac (#1603)

feat(data/nat): a lemma about min_fac (#1603) * feat(data/nat): a lemma about min_fac * feat(data/nat): a lemma about min_fac * use Rob's proof * fix * let's play golf * newline * use Chris' proof * cleaning up * rename per Chris' suggestions