proposition: Lemma compatible_ea f: function f -> compatible_with_equiv f (equivalence_associated f).
proof: Proof. move=> ff. have sr := proj2(graph_ea_equivalence ff). by split=> // x x' /(ea_relatedP ff) [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)