proposition: Lemma color4P x e : wf_color e -> color4_spec x e (x \in black e) (x \in stack e) (x \in cover (esccs e)) (x \in gray e) (x \in white e).
proof: Proof. move=> [/(_ x) s_def /subsetP /(_ x) /implyP]. move: s_def; rewrite whiteE grayE !inE. case x_black: (_ \in black _) => /=; case x_stack : (_ \in stack _) => /=; case x_sccs : (_ \in cover _) => //=; do ?by constructor. by constructor=> //; rewrite grayE !inE x_black. by constructor; rewrite whiteE grayE !inE x_black x_stack. Qed.
imports: mathcomp(all_ssreflect) bigmin extra