proposition: Lemma char_Zp : p > 1 -> p%:R = 0 :> 'Z_p.
proof: Proof. by move=> p_gt1; rewrite -Zp_nat_mod ?modnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)