proposition: Lemma stackP x e : wf_color e -> stack_spec x e (x \in white e) (x \in stack e) (x \in cover (esccs e)) (x \in gray e) (x \in black e).
proof: Proof. move=> e_cwf; set xb := x \in black _; set xg := x \in gray e. case: color4P => //. - by move=> /gray_stack; constructor. - by rewrite /xg /xb; case: color4P => //; constructor. - by rewrite /xg /xb; case: color4P => //; constructor. - by constructor. Qed.
imports: mathcomp(all_ssreflect) bigmin extra