proposition: Lemma Fp_cast : (Zp_trunc (pdiv p)).+2 = p.
proof: Proof. by rewrite Fp_Zcast ?Zp_cast ?prime_gt1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)