proposition: Lemma srestrict_sym (G : sgraph) (A : pred G) : connect_sym (restrict A (--)).
proof: Proof. exact/connect_symI/symmetric_restrict_sedge. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)