proposition: Lemma nat_of_ary_ub (s : seq 'I_t) : nat_of_ary s < t ^ size s.
proof: Proof. elim/last_ind : s => [|a b IH]; first by rewrite /nat_of_ary big_ord0 expn0. rewrite -{1}cats1 nat_of_ary_cat expn1 size_rcons /= card_ord. rewrite (@leq_trans (nat_of_ary a * t + t)) // ?ltn_add2l ?nat_of_ary1 //. by rewrite -mulSnr expnSr leq_pmul2r. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext