proposition: Lemma equivalence_relation_pr1 g: sgraph g -> equivalence_r (related g) -> equivalence g.
proof: Proof. move=> gg [sr tr]; apply: symmetric_transitive_equivalence => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)