proposition: Lemma add_1_Zp p (x : 'Z_p) : 1 + x = ordS x.
proof: Proof. by case: p => [|[|p]] in x *; apply/val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)