proposition: Lemma foq_induced_rel_fi: injection (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))).
proof: Proof. move: (ira)=> [er sa]. set (f := (canonical_injection a (substrate r))). have [ei sr] := (induced_rel_equivalence). have ff: function f by rewrite /f;apply: ci_f. have tf: target f = substrate r by rewrite /f /canonical_injection; aw. have sf: source f = substrate (induced_relation r a). by rewrite /f sr // /canonical_injection; aw. split; first by apply: foqcs_f. have ->: (source (fun_on_quotients (induced_relation r a) r f) = quotient (induced_relation r a) ). by rewrite/fun_on_quotients /section_canon_proj; aw. move=> x y xs ys /=; rewrite foqcs_V // foqcs_V //. have eq: a = substrate (induced_relation r a) by rewrite sr. have rxa: inc (rep x) a by rewrite eq; fprops. have rya: inc (rep y) a by rewrite eq; fprops. rewrite ci_V // ci_V // => cc. have: (related (induced_relation r a) (rep x) (rep y)). apply /induced_rel_relatedP; split => //; apply/ related_equiv_P => //. by split => //; apply: sa. by move /(related_rr_P ei xs ys). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)