michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/group_power,library/*): change definition of pow

Browse source 
I changed the definition of pow so that a^(succ n) reduces to a * a^n rather than a^n * a.

This has the nice effect that on nat and int, where multiplication is defined by recursion on the right,
a^1 reduces to a, and a^2 reduces to a * a.

The change was a pain in the neck, and in retrospect maybe not worth it, but oh, well.
This commit is contained in:
Jeremy Avigad 2015-08-14 11:00:16 -04:00 committed by Leonardo de Moura
parent f9f4cd2197
commit 4a36f843f7
10 changed files with 69 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/group_bigops.lean
View file

@ -84,7 +84,7 @@ section monoid
| (a::l) := take b, assume Pconst,
assert Pconstl : ∀ a', a' ∈ l → f a' = b,
from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in),
by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ' b]
by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ b]
end monoid

49
library/algebra/group_power.lean
View file

@ -26,30 +26,45 @@ include s
definition pow (a : A) : ℕ → A
| 0 := 1
| (n+1) := pow n * a
| (n+1) := a * pow n
infix [priority algebra.prio] `^` := pow
theorem pow_zero (a : A) : a^0 = 1 := rfl
theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a^n * a := rfl
theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a * a^n := rfl
theorem pow_succ' (a : A) : ∀n, a^(succ n) = a * a^n
theorem pow_one (a : A) : a^1 = a := !mul_one
theorem pow_two (a : A) : a^2 = a * a :=
calc
a^2 = a * (a * 1) : rfl
... = a * a : mul_one
theorem pow_three (a : A) : a^3 = a * (a * a) :=
calc
a^3 = a * (a * (a * 1)) : rfl
... = a * (a * a) : mul_one
theorem pow_four (a : A) : a^4 = a * (a * (a * a)) :=
calc
a^4 = a * a^3 : rfl
... = a * (a * (a * a)) : pow_three
theorem pow_succ' (a : A) : ∀n, a^(succ n) = a^n * a
| 0 := by rewrite [pow_succ, *pow_zero, one_mul, mul_one]
| (succ n) := by rewrite [pow_succ, pow_succ' at {1}, pow_succ, mul.assoc]
theorem one_pow : ∀ n : ℕ, 1^n = (1:A)
| 0 := rfl
| (succ n) := by rewrite [pow_succ, mul_one, one_pow]
| (succ n) := by rewrite [pow_succ, one_mul, one_pow]
theorem pow_one (a : A) : a^1 = a := !one_mul
theorem pow_add (a : A) (m : ℕ) : ∀ n, a^(m + n) = a^m * a^n
| 0 := by rewrite [nat.add_zero, pow_zero, mul_one]
| (succ n) := by rewrite [add_succ, *pow_succ, pow_add, mul.assoc]
theorem pow_add (a : A) (m n : ℕ) : a^(m + n) = a^m * a^n :=
begin
induction n with n ih,
{rewrite [nat.add_zero, pow_zero, mul_one]},
rewrite [add_succ, *pow_succ', ih, mul.assoc]
end
theorem pow_mul (a : A) (m : ℕ) : ∀ n, a^(m * n) = (a^m)^n
| 0 := by rewrite [nat.mul_zero, pow_zero]
| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ, pow_mul]
| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ', pow_mul]
theorem pow_comm (a : A) (m n : ℕ) : a^m * a^n = a^n * a^m :=
by rewrite [-*pow_add, nat.add.comm]
@ -65,7 +80,7 @@ include s
theorem mul_pow (a b : A) : ∀ n, (a * b)^n = a^n * b^n
| 0 := by rewrite [*pow_zero, mul_one]
| (succ n) := by rewrite [*pow_succ, mul_pow, *mul.assoc, mul.left_comm a]
| (succ n) := by rewrite [*pow_succ', mul_pow, *mul.assoc, mul.left_comm a]
end comm_monoid
@ -87,7 +102,7 @@ eq_mul_inv_of_mul_eq H2
theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
| 0 n := by rewrite [*pow_zero, one_mul, mul_one]
| m 0 := by rewrite [*pow_zero, one_mul, mul_one]
| (succ m) (succ n) := by rewrite [pow_succ at {1}, pow_succ' at {1}, pow_succ, pow_succ',
| (succ m) (succ n) := by rewrite [pow_succ' at {1}, pow_succ at {1}, pow_succ', pow_succ,
*mul.assoc, inv_mul_cancel_left, mul_inv_cancel_left, pow_inv_comm]
end nat
@ -143,7 +158,7 @@ theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : pow a n > 0 :=
induction n,
rewrite pow_zero,
apply zero_lt_one,
rewrite pow_succ,
rewrite pow_succ',
apply mul_pos,
apply v_0, apply H
end
@ -153,7 +168,7 @@ theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : pow a n ≥ 1 :=
induction n,
rewrite pow_zero,
apply le.refl,
rewrite [pow_succ, -{1}mul_one],
rewrite [pow_succ', -{1}mul_one],
apply mul_le_mul v_0 H zero_le_one,
apply le_of_lt,
apply pow_pos,
@ -163,7 +178,7 @@ theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : pow a n ≥ 1 :=
local notation 2 := (1 : A) + 1
theorem pow_two_add (n : ℕ) : pow 2 n + pow 2 n = pow 2 (succ n) :=
by rewrite [pow_succ, left_distrib, *mul_one]
by rewrite [pow_succ', left_distrib, *mul_one]
end ordered_ring
@ -180,9 +195,9 @@ definition nmul : ℕ → A → A := λ n a, pow a n
infix [priority algebra.prio] `⬝` := nmul
theorem zero_nmul (a : A) : (0:ℕ) ⬝ a = 0 := pow_zero a
theorem succ_nmul (n : ℕ) (a : A) : succ n ⬝ a = nmul n a + a := pow_succ a n
theorem succ_nmul (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ a n
theorem succ_nmul' (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ' a n
theorem succ_nmul' (n : ℕ) (a : A) : succ n ⬝ a = nmul n a + a := pow_succ' a n
theorem nmul_zero (n : ℕ) : n ⬝ 0 = (0:A) := one_pow n

10
library/algebra/ring_power.lean
View file

@ -22,14 +22,14 @@ theorem pow_pos_of_pos {x : A} (i : ℕ) (H : x > 0) : x^i > 0 :=
begin
induction i with [j, ih],
{show (1 : A) > 0, from zero_lt_one},
{show x^(succ j) > 0, from mul_pos ih H}
{show x^(succ j) > 0, from mul_pos H ih}
end
theorem pow_nonneg_of_nonneg {x : A} (i : ℕ) (H : x ≥ 0) : x^i ≥ 0 :=
begin
induction i with [j, ih],
{show (1 : A) ≥ 0, from le_of_lt zero_lt_one},
{show x^(succ j) ≥ 0, from mul_nonneg ih H}
{show x^(succ j) ≥ 0, from mul_nonneg H ih}
end
theorem pow_le_pow_of_le {x y : A} (i : ℕ) (H₁ : 0 ≤ x) (H₂ : x ≤ y) : x^i ≤ y^i :=
@ -37,8 +37,8 @@ begin
induction i with [i, ih],
{rewrite *pow_zero, apply le.refl},
rewrite *pow_succ,
have H : 0 ≤ y^i, from pow_nonneg_of_nonneg i (le.trans H₁ H₂),
apply mul_le_mul ih H₂ H₁ H
have H : 0 ≤ x^i, from pow_nonneg_of_nonneg i H₁,
apply mul_le_mul H₂ ih H (le.trans H₁ H₂)
end
theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 :=
@ -53,7 +53,7 @@ begin
induction i with [i, ih],
{exfalso, exact !nat.lt.irrefl ipos},
have xige1 : x^i ≥ 1, from pow_ge_one _ (le_of_lt xgt1),
rewrite [pow_succ', -mul_one 1, ↑has_lt.gt],
rewrite [pow_succ, -mul_one 1, ↑has_lt.gt],
apply mul_lt_mul xgt1 xige1 zero_lt_one,
apply le_of_lt xpos
end

14
library/data/finset/equiv.lean
View file

@ -48,11 +48,11 @@ private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n
iff.intro
(suppose succ n ∈ of_nat s,
assert odd (s div 2^(succ n)), from odd_of_mem_of_nat this,
have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ at this, div_div_eq_div_mul, mul.comm]; assumption,
have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ' at this, div_div_eq_div_mul, mul.comm]; assumption,
show n ∈ of_nat (s div 2), from mem_of_nat_of_odd this)
(suppose n ∈ of_nat (s div 2),
assert odd ((s div 2) div (2 ^ n)), from odd_of_mem_of_nat this,
assert odd (s div 2^(succ n)), by rewrite [pow_succ, mul.comm, -div_div_eq_div_mul]; assumption,
assert odd (s div 2^(succ n)), by rewrite [pow_succ', mul.comm, -div_div_eq_div_mul]; assumption,
show succ n ∈ of_nat s, from mem_of_nat_of_odd this)
private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s :=
@ -93,7 +93,7 @@ finset.induction_on s dec_trivial
assert a ≠ 0, from suppose a = 0, by subst a; contradiction,
begin
cases a with a, contradiction,
have odd (2*2^a), by rewrite [pow_succ at o, mul.comm]; exact o,
have odd (2*2^a), by rewrite [pow_succ' at o, mul.comm]; exact o,
have even (2*2^a), from !even_two_mul,
exact absurd `even (2*2^a)` `odd (2*2^a)`
end))),
@ -104,7 +104,7 @@ finset.induction_on s dec_trivial
match a with
| 0 := suppose a = 0, absurd this `a ≠ 0`
| (succ a') := suppose a = succ a',
have even (2^(succ a')), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
have even (2^(succ a')), by rewrite [pow_succ', mul.comm]; apply even_two_mul,
even_add_of_even_of_even this `even (to_nat s)`
end rfl
end)
@ -144,7 +144,7 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
finset.ext (λ x,
have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
| zero :=
have even (2^(succ n)), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
have even (2^(succ n)), by rewrite [pow_succ', mul.comm]; apply even_two_mul,
have aux₁ : odd (2^(succ n) + s) ↔ odd s, from iff.intro
(suppose odd (2^(succ n) + s), by_contradiction
(suppose ¬ odd s,
@ -172,7 +172,7 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
by subst m; apply mem_insert)
(suppose succ m ∈ of_nat s, finset.mem_insert_of_mem _ (iff.mp !succ_mem_of_nat this))),
calc
succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s) : by rewrite pow_succ
succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s) : by rewrite pow_succ'
... ↔ m ∈ of_nat ((2^n * 2 + s) div 2) : succ_mem_of_nat
... ↔ m ∈ of_nat (2^n + s div 2) : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm]
... ↔ m ∈ insert n (of_nat (s div 2)) : by rewrite ih
@ -258,7 +258,7 @@ begin
mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add]
end },
{ have a ∉ predimage s, from suppose a ∈ predimage s, absurd (succ_mem_of_mem_predimage this) nains,
rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ, add.comm,
rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ', add.comm,
add_mul_div_self (dec_trivial : 2 > 0), -ih, to_nat_insert this, add.comm] }
end

2
library/data/fintype/function.lean
View file

@ -94,7 +94,7 @@ lemma length_all_lists : ∀ {n : nat}, length (@all_lists_of_len A _ n) = (card
| (succ n) := calc length _ = card A * length (all_lists_of_len n) : length_cons_all
... = card A * (card A ^ n) : length_all_lists
... = (card A ^ n) * card A : nat.mul.comm
... = (card A) ^ (succ n) : pow_succ
... = (card A) ^ (succ n) : pow_succ'
end list_of_lists

24
library/data/nat/power.lean
View file

@ -42,58 +42,58 @@ theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
... = x^j * (1 + 1) : by rewrite [mul.left_distrib, *mul_one]
... = x^j * 2 : rfl
... ≤ x^j * x : mul_le_mul_left _ `x ≥ 2`
... = x^(succ j) : rfl
... = x^(succ j) : pow_succ'
-- TODO: eventually this will be subsumed under the algebraic theorems
theorem mul_self_eq_pow_2 (a : nat) : a * a = pow a 2 :=
show a * a = pow a (succ (succ zero)), from
by rewrite [*pow_succ, *pow_zero, one_mul]
by rewrite [*pow_succ, *pow_zero, mul_one]
theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b = c
| a 0 0 h₁ h₂ := rfl
| a (succ b) 0 h₁ h₂ :=
assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
assert 1 < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 < 1` !lt.irrefl
| a 0 (succ c) h₁ h₂ :=
assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
assert 1 < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 < 1` !lt.irrefl
| a (succ b) (succ c) h₁ h₂ :=
assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
assert pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
assert pow a b = pow a c, by rewrite [*pow_succ at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
by rewrite [pow_cancel_left h₁ this]
theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b
| a 0 h := by rewrite [pow_succ', pow_zero, mul_one, div_self (pos_of_ne_zero h)]
| a (succ b) h := by rewrite [pow_succ', mul_div_cancel_left _ (pos_of_ne_zero h)]
| a 0 h := by rewrite [pow_succ, pow_zero, mul_one, div_self (pos_of_ne_zero h)]
| a (succ b) h := by rewrite [pow_succ, mul_div_cancel_left _ (pos_of_ne_zero h)]
lemma dvd_pow : ∀ (i : nat) {n : nat}, n > 0 → i ∣ i^n
| i 0 h := absurd h !lt.irrefl
| i (succ n) h := by rewrite [pow_succ]; apply dvd_mul_left
| i (succ n) h := by rewrite [pow_succ']; apply dvd_mul_left
lemma dvd_pow_of_dvd_of_pos : ∀ {i j n : nat}, i ∣ j → n > 0 → i ∣ j^n
| i j 0 h₁ h₂ := absurd h₂ !lt.irrefl
| i j (succ n) h₁ h₂ := by rewrite [pow_succ]; apply dvd_mul_of_dvd_right h₁
| i j (succ n) h₁ h₂ := by rewrite [pow_succ']; apply dvd_mul_of_dvd_right h₁
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 :=
suppose p^(succ i) ∣ n,
assert p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl,
assert p^i ∣ p^(succ i), from by rewrite [pow_succ']; apply dvd_of_eq_mul; apply rfl,
dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n`
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
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 :=
begin
rewrite [pow_succ],
rewrite [pow_succ'],
apply coprime_mul_right,
exact coprime_pow_right n h,
exact h

6
library/theories/group_theory/cyclic.lean
View file

@ -140,7 +140,7 @@ mem_sep_of_mem !mem_univ
lemma mem_cyc (a : A) : ∀ {n : nat}, a^n ∈ cyc a
| 0 := cyc_has_one a
| (succ n) :=
begin rewrite pow_succ, apply cyc_mul_closed a, exact mem_cyc, apply self_mem_cyc end
begin rewrite pow_succ', apply cyc_mul_closed a, exact mem_cyc, apply self_mem_cyc end
lemma order_le {a : A} {n : nat} : a^(succ n) = 1 → order a ≤ succ n :=
assume Pe, let s := image (pow a) (upto (succ n)) in
@ -243,7 +243,7 @@ local infix ^ := algebra.pow
lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
| 0 := by rewrite [pow_zero]
| (succ k) := begin
assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ,
assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
rewrite [Psucc, pow_eq_mul],
apply eq_of_veq,
rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]
@ -368,7 +368,7 @@ eq_of_feq (funext take f, calc
lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i
| 0 := begin rewrite [pow_zero, ↑rotl_perm, perm_one, -eq_iff_feq], esimp, rewrite rotl_seq_zero end
| (succ i) := begin rewrite [pow_succ, rotl_perm_pow_eq, rotl_perm_mul, one_add] end
| (succ i) := begin rewrite [pow_succ', rotl_perm_pow_eq, rotl_perm_mul, one_add] end
lemma rotl_perm_pow_eq_one : (rotl_perm A n 1) ^ n = 1 :=
eq.trans rotl_perm_pow_eq (eq_of_feq begin esimp [rotl_perm], rewrite [↑rotl_fun, rotl_id] end)

2
library/theories/group_theory/pgroup.lean
View file

@ -384,7 +384,7 @@ theorem first_sylow_theorem {p : nat} (Pp : prime p) :
obtain J PJ, from cauchy_theorem Pp Ppdvd,
exists.intro (fin_coset_Union (cyc J))
(exists.intro _
(by rewrite [pow_succ', -PcardH, -PJ]; apply card_Union_lcosets))
(by rewrite [pow_succ, -PcardH, -PJ]; apply card_Union_lcosets))
end sylow

10
library/theories/number_theory/prime_factorization.lean
View file

@ -98,7 +98,7 @@ begin
assert n' < n,
by rewrite -this; apply mult_rec_decreasing pgt1 npos,
begin
rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ'], subst n,
rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ], subst n,
apply mul_dvd_mul !dvd.refl,
apply ih _ this
end)
@ -122,8 +122,8 @@ begin
{rewrite [pow_zero, one_mul, zero_add]},
have p > 0, from lt.trans zero_lt_one pgt1,
have psin_pos : p^(succ i) * n > 0, from mul_pos (!pow_pos_of_pos this) npos,
have p ∣ p^(succ i) * n, by rewrite [pow_succ', mul.assoc]; apply dvd_mul_right,
rewrite [mult_rec pgt1 psin_pos this, pow_succ, mul.right_comm, !mul_div_cancel `p > 0`, ih],
have p ∣ p^(succ i) * n, by rewrite [pow_succ, mul.assoc]; apply dvd_mul_right,
rewrite [mult_rec pgt1 psin_pos this, pow_succ', mul.right_comm, !mul_div_cancel `p > 0`, ih],
rewrite [add.comm i, add.comm (succ i)]
end
@ -143,7 +143,7 @@ obtain m (H : n div p^(mult p n) = p * m), from exists_eq_mul_right_of_dvd pdvd,
assert n = p^(succ (mult p n)) * m, from
calc
n = p^mult p n * (n div p^mult p n) : by rewrite (mul_div_cancel' !pow_mult_dvd)
... = p^(succ (mult p n)) * m : by rewrite [H, pow_succ, mul.assoc],
... = p^(succ (mult p n)) * m : by rewrite [H, pow_succ', mul.assoc],
have p^(succ (mult p n)) ∣ n, by rewrite this at {2}; apply dvd_mul_right,
have succ (mult p n) ≤ mult p n, from le_mult pgt1 npos this,
show false, from !not_succ_le_self this
@ -239,7 +239,7 @@ begin
{rewrite [pow_zero, mult_one_right]},
have qpos : q > 0, from pos_of_prime primeq,
have qipos : q^i > 0, from !pow_pos_of_pos qpos,
rewrite [pow_succ, mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq]
rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq]
end
theorem mult_prod_pow_of_not_mem {p : ℕ} (primep : prime p) {s : finset ℕ}

4
library/theories/number_theory/primes.lean
View file

@ -194,7 +194,7 @@ lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p
have 1 ≥ 2, by rewrite -this; apply ge_two_of_prime hp,
absurd this dec_trivial
| (succ n) hp hd :=
have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
have p ∣ (m^n)*m, by rewrite [pow_succ' at hd]; exact hd,
or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this)
(suppose p ∣ m^n, dvd_of_prime_of_dvd_pow hp this)
(suppose p ∣ m, this)
@ -226,7 +226,7 @@ lemma eq_one_or_dvd_of_dvd_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i
| 0 := take i, assume Pp, begin rewrite [pow_zero], intro Pdvd, apply or.inl (eq_one_of_dvd_one Pdvd) end
| (succ m) := take i, assume Pp, or.elim (coprime_or_dvd_of_prime Pp i)
(λ Pcp, begin
rewrite [pow_succ], intro Pdvd,
rewrite [pow_succ'], intro Pdvd,
apply eq_one_or_dvd_of_dvd_prime_pow Pp,
apply dvd_of_coprime_of_dvd_mul_right,
apply coprime_swap Pcp, exact Pdvd