From e63051118443a7a41a63fc9538593e161990c58f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Jul 2015 23:31:04 -0700
Subject: [PATCH] feat(library/data/nat/primes): add more simple theorems for
 primes

---
 library/data/nat/primes.lean | 51 +++++++++++++++++++++++++++++++++++-
 1 file changed, 50 insertions(+), 1 deletion(-)

diff --git a/library/data/nat/primes.lean b/library/data/nat/primes.lean
index 044bfe4bc..d5cca3211 100644
--- a/library/data/nat/primes.lean
+++ b/library/data/nat/primes.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 
 Prime numbers
 -/
-import data.nat.fact data.nat.bquant data.nat.power logic.identities
+import data.nat.fact data.nat.gcd data.nat.bquant data.nat.power data.nat.parity logic.identities
 open bool
 
 namespace nat
@@ -33,6 +33,18 @@ decidable_of_decidable_of_iff _ (prime_ext_iff_prime p)
 lemma ge_two_of_prime {p : nat} : prime p → p ≥ 2 :=
 assume h, obtain h₁ h₂, from h, h₁
 
+lemma not_prime_zero : ¬ prime 0 :=
+λ h, absurd (ge_two_of_prime h) dec_trivial
+
+lemma not_prime_one : ¬ prime 1 :=
+λ h, absurd (ge_two_of_prime h) dec_trivial
+
+lemma prime_two : prime 2 :=
+dec_trivial
+
+lemma prime_three : prime 3 :=
+dec_trivial
+
 lemma pred_prime_pos {p : nat} : prime p → pred p > 0 :=
 assume h,
 have h₁ : p ≥ 2, from ge_two_of_prime h,
@@ -110,4 +122,41 @@ have p_ge_n : p ≥ n, from by_contradiction
     absurd (le.trans p_ge_2 h₆) dec_trivial),
 exists.intro p (and.intro p_ge_n prime_p)
 
+lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
+λ h₁ h₂, by_contradiction (λ hn,
+  have he : even p, from even_of_not_odd hn,
+  obtain k (hk : p = 2*k), from exists_of_even he,
+  have h₂ : 2 ∣ p, by rewrite [hk]; apply dvd_mul_right,
+  or.elim (divisor_of_prime h₁ h₂)
+    (λ h : 2 = 1, absurd h dec_trivial)
+    (λ h : 2 = p, by subst h; exact absurd h₂ !lt.irrefl))
+
+lemma coprime_of_prime_of_not_dvd {p n : nat} : prime p → ¬ p ∣ n → coprime p n :=
+λ h₁ h₂,
+  assert d₁ : gcd p n ∣ p, from !gcd_dvd_left,
+  assert d₂ : gcd p n ∣ n, from !gcd_dvd_right,
+  or.elim (divisor_of_prime h₁ d₁)
+    (λ h : gcd p n = 1, h)
+    (λ h : gcd p n = p,
+      assert d₃ : p ∣ n, by rewrite -h; exact d₂,
+      by contradiction)
+
+lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n → p ∣ m ∨ p ∣ n :=
+λ h₁ h₂, by_contradiction (λ h,
+  obtain (n₁ : ¬ p ∣ m) (n₂ : ¬ p ∣ n), from iff.mp !not_or_iff_not_and_not h,
+  assert c₁ : coprime p m, from coprime_of_prime_of_not_dvd h₁ n₁,
+  assert n₃ : p ∣ n, from dvd_of_coprime_of_dvd_mul_left c₁ h₂,
+  by contradiction)
+
+lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m
+| 0 hp hd :=
+  assert h₁ : p = 1, from eq_one_of_dvd_one hd,
+  have h₂ : 1 ≥ 2, by rewrite -h₁; apply ge_two_of_prime hp,
+  absurd h₂ dec_trivial
+| (succ n) hp hd :=
+  have hd₁ : p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
+  or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp hd₁)
+    (λ h, dvd_of_prime_of_dvd_pow hp h)
+    (λ h, h)
+
 end nat