proposition: Lemma Zp_addNz : left_inverse Zp0 Zp_opp Zp_add.
proof: Proof. by move=> x; apply: val_inj; rewrite /= modnDml subnK ?modnn // ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)