proposition: Lemma Zp_cast : p > 1 -> (Zp_trunc p).+2 = p.
proof: Proof. by case: p => [|[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)