Thanks a lot for the advice. Both are good helpers.

I believe that the `rewrite (inj_eq val_inj)`

trick is essentially the same as using `eqP`

to turn the boolean equality into a propositional one and afterwards using `f_equal`

. Right?

Of course, this only works if `val`

is the only input that differs.

(For the record, of course the above suggestions cannot easily finish off the goal without requiring that `1 < p`

for the `p`

of `Zp`

holds .)

Sebastian Ertel has marked this topic as resolved.

Sebastian Ertel said:

Thanks a lot for the advice. Both are good helpers.

I believe that the`rewrite (inj_eq val_inj)`

trick is essentially the same as using`eqP`

to turn the boolean equality into a propositional one and afterwards using`f_equal`

. Right?

Of course, this only works if`val`

is the only input that differs.(For the record, of course the above suggestions cannot easily finish off the goal without requiring that

`1 < p`

for the`p`

of`Zp`

holds .)

Not exactly, it's converts boolean equality on subtypes into boolean equality on their value projections.

Ah yes, you are right. Thanks again for this clarification.

Thank very much for the answers.

@Paolo Giarrusso, yes, that was actually what I was trying to understand. It is not `case`

that "performs the computation" but actually the `by`

which executes `done`

.

I was able to "visualize" this for me by writing it more verbosely.

```
Lemma Zp1neqInZp0 : forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
case.
- move => //=.
- move => //=.
Qed.
```

Thanks a lot for your great help!

Sebastian Ertel has marked this topic as resolved.

You can also have a slow motion :

```
Lemma Zp1neqInZp0 : forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
case.
- rewrite -[1 < 0]/false.
by [].
- move=> n _.
rewrite -[_ != _]/(1 != 0 %[mod n.+2]).
rewrite -[1 %% _]/1.
rewrite -[0 %% _]/0.
by [].
Qed.
```

```
```

And without the case :

```
Lemma Zp1neqInZp0 : forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
move=> q Hq.
rewrite -[_ != _]/(1 != 0 %[mod q.+1]).
rewrite -[0 %% _]/0.
Fail rewrite -[1 %% _]/1.
Qed.
```

It is slow but certainly speeds up my understanding of things ;)

Thanks a lot!

Last updated: Jul 25 2024 at 16:02 UTC