proposition: Lemma ea_graph_on: graph_on (eq_rel_associated f) (source f) = equivalence_associated f.
proof: Proof. set_extens t. move /Zo_P => [/setX_P[pe _ _] [pb pc pd]]. rewrite - pe; apply /compg_pP; exists (Vf f (P t)) => //; first Wtac. apply/igraph_pP; rewrite pd; Wtac. move/compg_P => [pt [z pa /igraph_pP pb]]. have pc: inc (P t) (source f) by Wtac. have pd: inc (Q t) (source f) by Wtac. apply: Zo_i; first by apply /setX_P. by split => //; rewrite - (Vf_pr ff pa) - (Vf_pr ff pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)