proposition: Lemma induced_rel_equivalence: equivalence_on (induced_relation r a) a.
proof: Proof. move: (iirel_relation induced_rel_iirel_axioms). by rewrite/canonical_injection; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)