proposition: Lemma prefix_modn (s1 s2 : seq 'I_t) : prefix s1 s2 -> nat_of_ary s2 = nat_of_ary s1 * #|'I_t| ^ (size s2 - size s1) + nat_of_ary s2 %% #|'I_t| ^ (size s2 - size s1).
proof: Proof. case/prefixP => s3 H. rewrite -{1 2}(eqP H) nat_of_ary_cat size_cat (addnC (_ s1)) addnK; congr addn. rewrite -{1 2}(eqP H) nat_of_ary_cat size_cat (addnC (_ s1)) addnK. by rewrite modnMDl modn_small // card_ord nat_of_ary_ub. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext