proposition: Theorem equivalence_pr r: equivalence r <-> ((r \cg r) = r /\ r = inverse_graph r).
proof: Proof. split => hyp. move: (hyp) => [pa pb pc pd]. split; last by apply /selfinverse_graph_symmetric. apply: extensionality. by apply /idempotent_graph_transitive. move=> x xr; move: (pa _ xr) => px. rewrite - px; apply /compg_pP; exists (P x); rewrite ? px //. equiv_tac =>//; substr_tac. move: hyp=> [crr ri]. have gr: (sgraph r) by rewrite ri; fprops. apply: symmetric_transitive_equivalence => //. by apply /selfinverse_graph_symmetric. apply/idempotent_graph_transitive => //; rewrite crr; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)