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
```

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`

.

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

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`

.

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`

.

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

Recent threads on unicity of prime decomposition:

https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Unicity.20of.20prime.20decomposition

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/More.20like.20a.20math.20question.2C.20but.20still

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`

.

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

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

Last updated: Feb 08 2023 at 23:03 UTC