proposition: Lemma add_sccs_wf x e : take (index x (stack e)) (stack e) \subset black e -> x \in gray e -> wf_color e -> wf_color (add_sccs x e).
proof: Proof. move=> new_black x_gray e_wf. have [s_def /subsetP sccs_black s_uniq] := e_wf. split => //=; last first. - by rewrite (subseq_uniq (drop_subseq _ _)). - apply/subsetP=> y; rewrite !inE. rewrite /cover bigcup_setU inE big_set1 !inE /= => /orP[|/sccs_black->]; last by rewrite !orbT. by rewrite mem_rcons !inE; case: eqP => //= _ /(subsetP new_black). move=> y; rewrite !inE /cover bigcup_setU inE big_set1 !inE !negb_or. rewrite grayE ?inE //. have [->|neq_xy] //= := altP (y =P x); rewrite ?(andbT, andbF). case: path.splitP new_black s_uniq => //=; first by rewrite gray_stack. move=> s1 s2 s1x_black s_uniq; rewrite gray_sccsF // andbT. by rewrite (uniq_catRL s_uniq) // mem_cat mem_rcons mem_head. case: color4P; rewrite ?(andbT, andbF, orbT, orbF) //=. by move=> y_sccs; apply: contraTF y_sccs => /mem_drop; case: color4P. move=> y_black; case: path.splitP s_uniq; first by rewrite gray_stack. by move=> s1 s2 s_uniq y_in; apply: uniq_catRL. Qed.
imports: mathcomp(all_ssreflect) bigmin extra