proposition: Lemma ary_of_nat_unfold n : ary_of_nat n = if n < t then [:: inord n] else rcons (ary_of_nat (n %/ t)) (inord (n %% t)).
proof: Proof. rewrite {1}/ary_of_nat Fix_eq //. destruct n => //=. congr cons; apply val_inj => /=; by rewrite inordK. move=> m f f' H; congr ary_of_nat'. apply FunctionalExtensionality.functional_extensionality_dep => k. by apply FunctionalExtensionality.functional_extensionality. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext