proposition: Lemma size_ary_of_nat k : k != 0 -> forall n, n < t ^ k -> size (ary_of_nat n) <= k.
proof: Proof. elim: k.+1 {-2}k (ltnSn k) => // {}k IH [_ //|n]. rewrite ltnS => nk _ m mt. rewrite ary_of_nat_unfold; case: ifPn => //. rewrite -leqNgt => tm; rewrite size_rcons ltnS IH //. destruct n as [|n] => //. rewrite expn1 in mt; move: (leq_ltn_trans tm mt); by rewrite ltnn. by rewrite -(@ltn_pmul2r t) // -expnSr (leq_trans _ mt) // ltnS leq_trunc_div. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext