proposition: Lemma ea_relatedP x y: related (equivalence_associated f) x y <-> [/\ inc x (source f), inc y (source f) & Vf f x = Vf f y].
proof: Proof. rewrite - ea_graph_on; split; first by move/graph_on_P1 => [_ _]. by move =>[pa pb pc]; hnf; apply /graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)