feat(data/nat/factorization): add le_of_mem_factorization (#12032)

`le_of_mem_factors`: every factor of `n` is `≤ n`
`le_of_mem_factorization`: everything in `n.factorization.support` is `≤ n`

Author: stuart-presnell

src/data/nat/factorization.lean

@@ -79,6 +79,9 @@ prime_of_mem_factors ∘ (@factor_iff_mem_factorization n p).mp
 lemma pos_of_mem_factorization {n p : ℕ} : p ∈ n.factorization.support → 0 < p :=
 prime.pos ∘ (@prime_of_mem_factorization n p)
 
+lemma le_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ≤ n :=
+le_of_mem_factors (factor_iff_mem_factorization.mp h)
+
 lemma factorization_eq_zero_of_non_prime (n p : ℕ) (hp : ¬p.prime) : n.factorization p = 0 :=
 not_mem_support_iff.1 (mt prime_of_mem_factorization hp)
 

src/data/nat/prime.lean

@@ -696,6 +696,13 @@ lemma mem_factors {n p} (hn : n ≠ 0) : p ∈ factors n ↔ prime p ∧ p ∣ n
 ⟨λ h, ⟨prime_of_mem_factors h, (mem_factors_iff_dvd hn $ prime_of_mem_factors h).mp h⟩,
  λ ⟨hprime, hdvd⟩, (mem_factors_iff_dvd hn hprime).mpr hdvd⟩
 
+lemma le_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) : p ≤ n :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn,
+  { rw factors_zero at h, cases h },
+  { exact le_of_dvd hn (dvd_of_mem_factors h) },
+end
+
 /-- **Fundamental theorem of arithmetic**-/
 lemma factors_unique {n : ℕ} {l : list ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, prime p) :
   l ~ factors n :=