proposition: Lemma sub_Zp_1 p (x : 'Z_p) : x - 1 = ord_pred x.
proof: Proof. by apply: (addIr 1); rewrite addrNK add_Zp_1 ord_predK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)