no goals
m k n : Nat
H1 : coprime m k
⊢ coprime (m ^ n) k
induction n with
| zero => exact coprime_one_left _
| succ n ih => have hm := H1.mul ih; rwa [Nat.pow_succ, Nat.mul_comm]
no goals
case zero
m k : Nat
H1 : coprime m k
⊢ coprime (m ^ zero) k
exact coprime_one_left _
case succ
m k : Nat
H1 : coprime m k
n : Nat
ih : coprime (m ^ n) k
hm : coprime (m * m ^ n) k
⊢ coprime (m ^ succ n) k
case succ
m k : Nat
H1 : coprime m k
n : Nat
ih : coprime (m ^ n) k
⊢ coprime (m ^ succ n) k
have hm := H1.mul ih
no goals
case succ
m k : Nat
H1 : coprime m k
n : Nat
ih : coprime (m ^ n) k
hm : coprime (m * m ^ n) k
⊢ coprime (m ^ succ n) k
rwa [Nat.pow_succ, Nat.mul_comm]