proposition: Lemma nat_of_ary_0' s : nat_of_ary s = 0 -> all (eq_op^~ ord0) s.
proof: Proof. elim: s => // a b IH. rewrite -cat1s nat_of_ary_cat => /eqP; rewrite addn_eq0 => /andP[/=]. rewrite muln_eq0 card_ord expn_eq0 /= orbF nat_of_ary1 => /eqP H1 /eqP H2. by rewrite /= IH // andbT; apply/eqP/val_inj. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext