How can one do a case analysis on the possible values of some x modulo some d ? For instance, say I want to check that x^2 %% 8 is never 7, and do so by just checking the 8 possible cases for (x %% 8) ? (x %% d) has type nat and not some finite Type, but on the other hand the fact that x %% d < d is in the library, so perhaps one could use this together with induction on nat? Is there some more elegant way to proceed?

I would do something like

```
by move: n (ltn_mod n 8); do 8![case=> //].
```

(no need for induction here, you want to explore a finite number of cases exhaustively)

Thanks! I see how `do 8![case=> //].`

does the first 8 cases in `n`

. But it doesn't conclude (on the trivial example of x^2 %% 8 not being 7). I still need to check: `n.+4.+4 ^ 2 %% 8 <> 7`

. So it didn't use `ltn_mod n 8`

to see that there were only these 8 cases to check... How do I help it conclude?

I guess it could do the case analysis on the possible values of `n %% 8`

, check the first 8 cases with some help to deduce `n^2 %% 8`

, and then dismiss the other cases thanks to `ltn_mod`

?

Oh yes sorry, it is slightly more complicated... I did not open Coq to try it before sending you the message

One would need to substitute `n`

for `n %% 8`

in the goal.

`by rewrite -modnXm; move: (n %% 8) (ltn_mod n 8); do 8![case=> //].`

```
From mathcomp Require Import all_ssreflect.
Lemma test n : n ^ 2 %% 8 != 7.
by rewrite -modnXm; move: (n %% 8) (ltn_mod n 8); do 8![case=> //].
Qed.
```

Oh, excellent. Thank you very much!

Last updated: Jul 25 2024 at 16:02 UTC