proposition: Lemma compatible_injection_induced_rel: compatible_with_equivs (canonical_injection a (substrate r)) (induced_relation r a) r.
proof: Proof. move: (ira)=> [er sa]. move:(induced_rel_equivalence) => [qa qb]. apply: compatible_with_pr2 =>//. - by apply: ci_f. - by rewrite/canonical_injection; aw. - by rewrite/canonical_injection;aw. - move=> x y /induced_rel_relatedP [xa ya rxy]; rewrite ci_V // ci_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)