proposition: Lemma modZp_pow m n : inZp (m %% 2 ^ n.+1) = inZp (p' := (Zp_trunc (2^n.+1)).+1) m.
proof: Proof. apply val_inj. simpl. rewrite prednK. rewrite prednK. by rewrite modn_mod. apply expn_gt0. have P:= pow2_gt1 n. rewrite -(ltn_add2r 1). rewrite !addn1 prednK. done. apply expn_gt0. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)