proposition: Lemma suffixes_not_empty (i : 'I_n) : 0 < #|T| -> suffixes (nth [::] C i) <> set0.
proof: Proof. move=> T0. rewrite /suffixes mem_nth //. move/setP. have [t Ht] : exists t : T, t \in T by move/card_gt0P : T0. move/(_ (@prepend T lmax (nth [::] C i) [tuple of nseq _ t])). rewrite !inE /prepend /= take_oversize ?prefix_cat //. apply/leq_lmax/(nthP [::]); by exists i. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext