proposition: Lemma nat_of_ary_nseq0 (n : nat) : nat_of_ary (nseq n ord0) = 0.
proof: Proof. rewrite /nat_of_ary (eq_bigr (fun=> O)) ?big1 //= => i _. rewrite nth_nseq; by case: ifPn. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext