theorem Nat.coprime_pow_two_of_odd {p k : Nat} (hp : p % 2 = 1) : p.Coprime (2 ^ k)

An odd number is coprime to every power of two. Montgomery inversion uses this exact named lemma to discharge the Nat.Coprime p (2 ^ k) side condition for the radix R = 2^k.