## Stream: Coq users

### Topic: Discharging power mod proof

#### Mukesh Tiwari (Jul 16 2022 at 21:21):

Hi Everyone, is there an easy way to discharge this proof? (One idea that I am thinking is generalising the lemma and replacing `pt - 2` by `n` and induction on `n` but I haven't tried it).

``````Lemma power_mod :
forall (pt : Z),
prime pt ->
forall au,
0 < au < pt ->
0 < au ^ (pt - 2) mod pt.
Proof.
intros * Hw ? [Ha Hb].
assert (Ht : 0 <= pt - 2).
nia.
pose proof Z.pow_pos_nonneg au (pt - 2) Ha Ht as Hpp.

p: Z
Hp: prime p
pt: Z
Hw: prime pt
au: Z
Ha: 0 < au
Hb: au < pt
Ht: 0 <= pt - 2
Hpp: 0 < au ^ (pt - 2)
1/1
0 < au ^ (pt - 2) mod pt
``````

#### Paolo Giarrusso (Jul 16 2022 at 22:10):

do you have Fermat's little theorem available? https://en.wikipedia.org/wiki/Fermat%27s_little_theorem. From that and the properties of modular arithmetic, it follows (informally) that au ^ (pt - 2) = au^-1 mod pt, and since `pt` is prime and does not divide `au`, `au^-1` can't be `0`.

#### Paolo Giarrusso (Jul 16 2022 at 22:11):

so I guess I'm assuming that theorem _and_ the surrounding theory

#### Paolo Giarrusso (Jul 16 2022 at 22:20):

One idea that I am thinking is generalising the lemma and replacing pt - 2 by n and induction on n but I haven't tried it

That might be a simpler idea, once you import a proof of unicity of prime decompositions — but once again I'll stick to an informal sketch. As a corollary of unique prime decomposition, you have that if a prime `pt` doesn't divide `au`, `pt` cannot divide`au^n`, so `au^n mod pt > 0`.

#### Paolo Giarrusso (Jul 16 2022 at 22:22):

And some fancy arith is necessary, because the theorem is false without the `prime pt` assumption: setting `au = 2`, `pt = 4` gives `au ^ (pt - 2) mod pt = 2 ^ (4 - 2) mod 4 = 0`.

#### Paolo Giarrusso (Jul 16 2022 at 22:22):

"fancy arith" = relying on the theory of primality.

#### Paolo Giarrusso (Jul 16 2022 at 22:31):

As a corollary of unique prime decomposition, you have that if a prime `pt` doesn't divide `au`, `pt` cannot divide`au^n`, so `au^n mod pt > 0`.

The proof proceeds by contradiction: we assume that `pt` divides`au^n`, and prove that `pt` divides `au`. We can do this constructively since divisibility is decidable. Now, `au` can be written as `\Pi_i p_i^a_i` where `p_i` is the sequence of primes and `a_i` are suitable coefficients. Then `au^n = \Pi_i p_i^(a_i * n)`. Since `pt` is prime there is a `j` such that `pt = p_j`; then `pt | au^n` means that `a_j * n > 0` so `a_j > 0`, hence `pt` divides `au`! But that contradicts `0 < au < pt`, so `pt` cannot divide`au^n`.

#### Mukesh Tiwari (Jul 17 2022 at 08:23):

Thank you very much @Paolo Giarrusso . Yeah, I have Fermat's little theorem available.

#### Karl Palmskog (Jul 17 2022 at 09:34):

I think the final step is more technically a proof of negation

Last updated: Sep 30 2023 at 06:01 UTC