proposition: Lemma graph_ea_equivalence: equivalence_on (equivalence_associated f) (source f).
proof: Proof. rewrite - ea_graph_on; split; last by rewrite graph_on_sr. apply: equivalence_from_rel; split. by move => a b [pa pb pc]. move => a b c [pa pb pc] [pd pe pf]; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)