From 5034de9c4e1f7558a73ccb94fe8967830e864034 Mon Sep 17 00:00:00 2001
From: Haitao Zhang <zhtprog@gmail.com>
Date: Mon, 13 Jul 2015 14:51:35 -0700
Subject: [PATCH] feat(library/data/nat/power): add nat power divide theorems

---
 library/data/nat/order.lean | 3 +++
 library/data/nat/power.lean | 9 +++++++++
 2 files changed, 12 insertions(+)

diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 1f2212ee9..afb430460 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -313,6 +313,9 @@ discriminate
 theorem lt_succ_self (n : ℕ) : n < succ n :=
 lt.base n
 
+lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
+assume Plt, lt.trans Plt (self_lt_succ j)
+
 /- other forms of induction -/
 
 protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) :
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index 3a26bb448..324b79eae 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -80,6 +80,15 @@ lemma dvd_pow_of_dvd_of_pos : ∀ {i j n : nat}, i ∣ j → n > 0 → i ∣ j^n
 lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i^n) mod i = 0 :=
 iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h)
 
+lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n :=
+assume Psuccdvd,
+assert Pdvdsucc : p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl,
+dvd.trans Pdvdsucc Psuccdvd
+
+lemma dvd_of_pow_succ_dvd_mul_pow {p i n : nat} (Ppos : p > 0) :
+  p^(succ i) ∣ (n * p^i) → p ∣ n :=
+by rewrite [pow_succ']; apply dvd_of_mul_dvd_mul_right; apply pow_pos_of_pos _ Ppos
+
 lemma coprime_pow_right {a b} : ∀ n, coprime b a → coprime b (a^n)
 | 0        h := !comprime_one_right
 | (succ n) h :=