proposition: Lemma symmetric_transitive_equivalence r: sgraph r -> symmetricp r -> transitivep r -> equivalence r.
proof: Proof. move=> gr sr tr; hnf; split => //. move => y /(substrate_P gr) [][z pr]. apply: (tr _ _ _ pr (sr _ _ pr)). apply: (tr _ _ _ (sr _ _ pr) pr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)