I need to prove the following goal:

```
p : nat
p_pr : prime p
a, b : 'Z_(p ^ 1)
============================
a != 0 -> b != 0 -> a * b != 0
```

The command

```
rewrite expn1 in a b |- *.
```

allows to easily get rid of the `p ^ 1`

. Now I would like MC to understand that I'm in `'F_p`

, I try to do

```
rewrite -(Fp_Zcast p_pr) in a b |- *.
```

And it leads to a dependent type error. How can I solve this problem ? I can try to use the ismorphism

```
have eq_p := (Fp_Zcast p_pr); pose f := cast_ord (esym eq_p).
```

but now I need to prove that `f`

is a ring morphism. I find it currently painful. Is there simpler way ?

Indeed! If you redefine `Fp_Zcast`

it works, I think this should be fixed in mc.

```
Lemma Fp_Zcast [p : nat] : prime p -> Zp_trunc (pdiv p) = Zp_trunc p.
Proof. by move=> /Fp_Zcast[[]]. Qed.
Lemma test (p : nat) (p_pr : prime p) (a b : 'Z_(p ^ 1)) :
a != 0 -> b != 0 -> a * b != 0.
Proof.
rewrite -Fp_Zcast // in a b *.
exact: mulf_neq0.
Qed.
```

Cyril Cohen said:

Indeed! If you redefine

`Fp_Zcast`

it works, I think this should be fixed in mc.`Lemma Fp_Zcast [p : nat] : prime p -> Zp_trunc (pdiv p) = Zp_trunc p. Proof. by move=> /Fp_Zcast[[]]. Qed. ```` Neat ! I'm sumbitting a pull request !`

Cyril Cohen has marked this topic as resolved.

Last updated: Jul 15 2024 at 21:02 UTC