proposition: Lemma symmetric_restrict_sedge (G : sgraph) (A : pred G) : symmetric (restrict A (--)).
proof: Proof. apply: restrict_sym. exact: sg_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)