proposition: Lemma iirel_relation f r: iirel_axioms f r -> equivalence_on (inv_image_relation f r) (source f).
proof: Proof. by move=> ia;move:(graph_ea_equivalence(iirel_f ia)); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)