Results on gcd

Stream: Is there code for X?

[Victor Tsynkov]

Not sure if this thread if for such questions: is there anywhere in mathlib a proof of something like this example below? If not, what is the easiest way to get this? I tried library_search with no success. Or am I missing some obvious fact here?

example (n m : ℕ) (h : nat.gcd n m = 1) : nat.gcd (n ^ 2) m = 1 :=
begin
    sorry,
end

[Johan Commelin]

I don't know by heart, but I guess this is a lemma about nat.coprime

[Victor Tsynkov]

@Johan Commelin Thanks. With your input, I see that I can get it from nat.coprime.mul.
But a more general variant for arbitrary powers is still not obvious.

[Johan Commelin]

If nat.coprime.pow doesn't exist, then you can write it. It's 3 lines if you use nat.coprime.mul.

[Yury G. Kudryashov]

It should be nat.coprime.pow_left, pow_right, and pow_pow.

[Mario Carneiro]

I'm pretty sure this exists

[Mario Carneiro]

nat.coprime.pow_left, exactly

[Mario Carneiro]

pow_pow is actually just called nat.coprime.pow