proposition: Lemma cat3_equiv_cut3 s a b c : s == a ++ b ++ c <-> (a, b, c) \in cut3 s.
proof: Proof. Proof using. have -> : (a ++ b ++ c) = flatten [:: a; b; c] by rewrite /= cats0. rewrite flatten_equiv_cut_k /cut3; split. - by move=> H; apply/mapP; exists [:: a; b; c]. - move=> /mapP[t]. case: t => [| t0 t]; first by rewrite /cut_k => /size_cut_k. case: t => [| t1 t]; first by rewrite /cut_k => /size_cut_k. case: t => [| t2 t]; first by rewrite /cut_k => /size_cut_k. case: t => [| t3 t]; last by rewrite /cut_k => /size_cut_k. by move=> Hcut [-> -> ->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools