proposition: Lemma Zp_mulVz x : coprime p x -> Zp_mul (Zp_inv x) x = Zp1.
proof: Proof. move=> co_p_x; apply: val_inj; rewrite /Zp_inv co_p_x /= modnMml. by rewrite -(chinese_modl co_p_x 1 0) /chinese addn0 mul1n mulnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)