proposition: Lemma closed_connect (T : finType) (e : rel T) (A : pred T) : closed e A -> {in A, subrel (connect e) (connect (restrict A e))}.
proof: Proof. move => clA x xA y. case/connectP => p; elim: p x xA => [x _ _ -> //|z p IHp /= x xA /andP [xz pth_p] lst_p]. have zA: z \in A by rewrite -(clA _ _ xz). by apply: connect_trans (IHp _ zA pth_p lst_p); apply:connect1; rewrite /= xA zA. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)