proposition: Lemma card_suffixes (c : seq T) : c \in C -> #| suffixes c | = #|T| ^ (lmax - size c).
proof: Proof. move=> cC. rewrite /suffixes cC -card_tuple -(card_imset _ (@injective_prepend T lmax c)). apply eq_card => /= t; rewrite !inE. apply/idP/imsetP => /= [ct|/= [x _ ->{t}]]. have @x : (lmax - size c).-tuple T. apply: (@Tuple _ _ (drop (size c) t)); by rewrite size_drop size_tuple. exists x => //; apply val_inj => /=. move: ct => /eqP {1}->. rewrite take_oversize ?cat_take_drop //. rewrite size_take size_tuple; by case: ifPn => // /ltnW. by rewrite /prepend /= take_oversize ?prefix_cat // leq_lmax. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext