fact: Fixpoint modnp_pow (n k : nat) (p : positive) (v : seq nat) := if p is xO p1 then let r := modnp_pow n k p1 v in modnp_mul n k r r else if p is xI p1 then let r := modnp_pow n k p1 v in modnp_mul n k v (modnp_mul n k r r) else v.
imports: mathcomp(all_ssreflect)