proposition: Lemma vs_disjoint : [disjoint stack e & cover (esccs e)].
proof: Proof. rewrite -setI_eq0; apply/eqP/setP=> x; rewrite !inE -num_sccs//. by rewrite -num_lt_V; case: ltngtP. Qed.
imports: mathcomp(all_ssreflect) bigmin extra