proposition: Lemma is_subscc1 x (A : {set V}) : x \in A -> (forall y, y \in A -> connect r x y /\ connect r y x) -> is_subscc A.
proof: Proof. move=> xA AP; split; first by apply: contraTneq xA => ->; rewrite inE. by move=> y z /AP [xy yx] /AP [xz zx]; rewrite (connect_trans yx). Qed.
imports: HB(structures) mathcomp(all_ssreflect)