proposition: Lemma ary_of_natK n : nat_of_ary (ary_of_nat n) = n.
proof: Proof. elim: n.+1 {-2}n (ltnSn n) => {n}// n IH m mn. rewrite ary_of_nat_unfold. case: ifPn => [nt|]; first by rewrite nat_of_ary1 inordK. rewrite -leqNgt => tn. rewrite -cats1 nat_of_ary_cat /= expn1 card_ord IH //; last first. rewrite ltn_divLR // (leq_trans mn) // ltn_Pmulr //. destruct n => //; by destruct m. by rewrite nat_of_ary1 inordK // ?ltn_pmod // -divn_eq. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext