proposition: Lemma ary_of_nat_head' n def : head def (ary_of_nat n.+1) != ord0.
proof: Proof. elim: n.+1 {-2}n (ltnSn n) def => {n}// n IH m; rewrite ltnS => mn def. rewrite ary_of_nat_unfold; case: ifPn => [nt /=|]. apply/eqP => /(congr1 val) /=; by rewrite inordK. rewrite -leqNgt => nt; rewrite headI /=. move: nt; rewrite leq_eqVlt => /orP[/eqP tm|]. rewrite (_ : _ %/ _ = 1); last by rewrite tm divnn. apply/eqP => /(congr1 val) /=; by rewrite inordK. move=> nt. suff [k Hk] : exists k : 'I_n, m.+1 %/ t = k.+1 by rewrite Hk IH. move=> [:Hx]. have @x : 'I_n. apply: (@Ordinal _ (m.+1 %/ t).-1 _). abstract: Hx. rewrite prednK ?divn_gt0 //; [apply/ltnW | by rewrite ltnW]. rewrite ltn_divLR // -addn2 mulnS leq_add //. destruct m as [|m] => //; destruct n as [|n] => //. rewrite mulnS addSn ltnS. destruct n as [|n]; by [destruct m | rewrite addSn ltnS]. by exists x => /=; rewrite prednK // divn_gt0 // ltnW. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext