Ssreflect Users Discussion List

[georges gonthier <>]

   That particular theorem actually holds in ‘Z_p, or indeed any 
unitRingType. While ssralg only supplies a contrapositive
   unitr0 : (0 \is a GRing.unit) = false
this is readily composed with one of the general contraposition lemmas, e.g.,
  apply/memPn: m; rewrite unitr0
For your general problem, Laurent has the right solution as ‘F_p is merely 
notation for ‘Z_(pdiv p).
If it’s inconvenient to rewrite the types as suggested, you may use
  cast_ord (esym (Fp_Zcast p_pr)) m
instead of m to gain access to the ‘F_p field theory.

   Georges

> Le 26 sept. 2019 à 10:43, Laurent Thery 
> <>
>  a écrit :
> 
> 
> 
> On 9/26/19 9:09 AM, Florent Hivert wrote:
>>      Dear All,
>> 
>> I've got the following goal:
>> 
>>  p : nat
>>  p_pr : prime p
>>  m : 'Z_p
>>  ============================
>>  m \is a GRing.unit -> m != 0
>> 
>> If I had "m : 'F_p" instead, i'd got it immediately thanks to unitfE.
>> 
> 
> One way to do this is to explicitly mention the m that needs to be
> rewritten.
> 
> rewrite -(pdiv_id Hp) in m |- *.
> 
> --
> Laurent
>