proposition: Lemma in_connect_sym (T : finType) (e : rel T) (A : pred T) : closed e A -> connect_sym e -> {in A&, connect_sym (restrict A e)}.
proof: Proof. move => clA sym_e x y xA yA. wlog suff : x y xA yA / connect (restrict A e) x y -> connect (restrict A e) y x. { by move => W; apply/idP/idP; apply: W. } case/connectP => p; elim: p x xA => /= [x _ _ -> //| z p IHp x xA]. rewrite -!andbA => /and4P [_ zA x_z pth_p lst_p]. have {pth_p lst_p} IH := IHp _ zA pth_p lst_p. apply: connect_trans IH _. have := (connect1 x_z); rewrite sym_e; exact: closed_connect. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)