proposition: Lemma ary_of_nat_head n def : (head def (ary_of_nat n) == ord0) = (n == O).
proof: Proof. apply/idP/idP => [|/eqP ->]; last by rewrite ary_of_nat0. apply: contraTT; destruct n as [|n] => // _; by apply ary_of_nat_head'. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext