proposition: Lemma nat_of_ary_0 s : (nat_of_ary s == 0) = (all (xpred1 ord0) s).
proof: Proof. apply/idP/idP => [/eqP|/all_pred1P H]; first exact: nat_of_ary_0'. apply/eqP/injective_ary_of_nat. by rewrite ary_of_nat0 H nat_of_ary_nseq0 ary_of_nat0. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext