proposition: Lemma disjoint_suffixes (a b : seq T) (Hprefix : prefix_code C) : a \in C -> b \in C -> a != b -> suffixes a :&: suffixes b == set0.
proof: Proof. move=> aC bC ab; rewrite /suffixes aC bC. apply/set0Pn => -[/= s]; rewrite !inE => /andP[sa sb]. wlog : a b aC bC sa sb ab / prefix a b. move=> H. case: (prefix_common sa sb) => K; first exact: (H _ _ aC bC). apply: (H _ _ bC aC sb sa _ K); by rewrite eq_sym. move/negP : (Hprefix _ _ aC bC ab); exact. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext