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

src/data/nat/basic.lean

@@ -1168,13 +1168,11 @@ dvd_trans this hdiv
 lemma dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p^k ∣ m) : p ∣ m :=
 by rw ←nat.pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
-lemma eq_of_dvd_quot_one {a b : ℕ} (w : a ∣ b) (h : b / a = 1) : a = b :=
-begin
-  rcases w with ⟨b, rfl⟩,
-  rw [nat.mul_comm, nat.mul_div_cancel] at h,
-  { simp [h] },
-  { by_contradiction, simp * at * }
-end
+lemma eq_of_dvd_of_div_eq_one {a b : ℕ} (w : a ∣ b) (h : b / a = 1) : a = b :=
+by rw [←nat.div_mul_cancel w, h, one_mul]
+
+lemma eq_zero_of_dvd_of_div_eq_zero {a b : ℕ} (w : a ∣ b)  (h : b / a = 0) : b = 0 :=
+by rw [←nat.div_mul_cancel w, h, zero_mul]
 
 lemma div_le_div_left {a b c : ℕ} (h₁ : c ≤ b) (h₂ : 0 < c) : a / b ≤ a / c :=
 (nat.le_div_iff_mul_le _ _ h₂).2 $

src/data/nat/prime.lean

@@ -213,6 +213,23 @@ section min_fac
   (not_congr $ prime_def_min_fac.trans $ and_iff_right n2).trans $
     (lt_iff_le_and_ne.trans $ and_iff_right $ min_fac_le $ le_of_succ_le n2).symm
 
+  lemma min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬ prime n) : min_fac n ≤ n / min_fac n :=
+  match min_fac_dvd n with
+  | ⟨0, h0⟩     := absurd pos $ by rw [h0, mul_zero]; exact dec_trivial
+  | ⟨1, h1⟩     :=
+    begin
+      rw mul_one at h1,
+      rw [prime_def_min_fac, not_and_distrib, ← h1, eq_self_iff_true, not_true, or_false, not_le] at np,
+      rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), min_fac_one, nat.div_one]
+    end
+  | ⟨(x+2), hx⟩ :=
+    begin
+      conv_rhs { congr, rw hx },
+      rw [nat.mul_div_cancel_left _ (min_fac_pos _)],
+      exact min_fac_le_of_dvd dec_trivial ⟨min_fac n, by rwa mul_comm⟩
+    end
+  end
+
 end min_fac
 
 theorem exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬ prime n) :