proposition: Lemma sigmaE0 : sigma ord0 = nseq (nth O l O) ord0 :> seq T.
proof: Proof. rewrite /sigma wE0 ary_of_nat0. have [k Hk] : exists k, nth 0 l (@ord0 t) = k.+1. move: (Hl ord0); case: (nth 0 l ord0) => // k _; by exists k. by rewrite Hk subn1 cat_nseq -[RHS]cats0 cat_nseq /= /ncons -iterSr. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext