proposition: Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x.
proof: Proof. case=> yx1; have:= coprimen1 p. by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)