proposition: Lemma size_sigma (i : 'I_n) : w i < t ^ nth O l i -> size (sigma i) = nth O l i.
proof: Proof. move=> step1; by rewrite /sigma size_cat size_nseq subnK // size_ary_of_nat. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext