proposition: Lemma natr_negZp (x : 'I_p) : (- x)%:R = - x.
proof: Proof. by apply: val_inj; rewrite /= Zp_nat /= modn_mod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)