feat(data/nat/prime): eq_prime_pow_of_dvd_least_prime_pow (#2791)

Proves
```lean
lemma eq_prime_pow_of_dvd_least_prime_pow
  (a p k : ℕ) (pp : prime p) (h₁ : ¬(a ∣ p^k)) (h₂ : a ∣ p^(k+1)) :
  a = p^(k+1)
```

Author: kim-em

src/data/nat/basic.lean

@@ -957,6 +957,25 @@ strict_mono.lt_iff_lt (pow_right_strict_mono k)
 lemma pow_right_injective {x : ℕ} (k : 2 ≤ x) : function.injective (nat.pow x) :=
 strict_mono.injective (pow_right_strict_mono k)
 
+lemma pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : Π {x : ℕ} (w : 0 < x), x^k ∣ x^l ↔ x^k ≤ x^l
+| (x+1) w :=
+begin
+  split,
+  { intro a, exact le_of_dvd (pow_pos (succ_pos x) l) a, },
+  { intro a, cases x with x,
+    { simp only [one_pow], },
+    { have le := (pow_le_iff_le_right (le_add_left _ _)).mp a,
+      use (x+2)^(l-k),
+      rw [←nat.pow_add, add_comm k, nat.sub_add_cancel le], } }
+end
+
+/-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`. -/
+lemma pow_dvd_pow_iff_le_right {x k l : ℕ} (w : 1 < x) : x^k ∣ x^l ↔ k ≤ l :=
+by rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_iff_le_right w]
+
+lemma pow_dvd_pow_iff_le_right' {b k l : ℕ} : (b+2)^k ∣ (b+2)^l ↔ k ≤ l :=
+pow_dvd_pow_iff_le_right (nat.lt_of_sub_eq_succ rfl)
+
 lemma pow_left_strict_mono {m : ℕ} (k : 1 ≤ m) : strict_mono (λ (x : ℕ), x^m) :=
 λ _ _ h, pow_lt_pow_of_lt_left h k
 

src/data/nat/prime.lean

@@ -460,6 +460,20 @@ begin
       rw e, exact pow_dvd_pow _ l } }
 end
 
+/--
+If `p` is prime,
+and `a` doesn't divide `p^k`, but `a` does divide `p^(k+1)`
+then `a = p^(k+1)`.
+-/
+lemma eq_prime_pow_of_dvd_least_prime_pow
+  {a p k : ℕ} (pp : prime p) (h₁ : ¬(a ∣ p^k)) (h₂ : a ∣ p^(k+1)) :
+  a = p^(k+1) :=
+begin
+  obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂,
+  congr,
+  exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (prime.one_lt pp))).1 h₁)),
+end
+
 section
 open list