proposition: Lemma vcoverP : reflect (forall x y, x -- y -> (x \in V) \/ (y \in V)) vcover.
proof: Proof. apply: (equivP idP). rewrite /vcover -(rwP forallP). setoid_rewrite <- (rwP forall_inP). by setoid_rewrite <- (rwP orP). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)