proposition: Lemma quo_rel_relatedP x y: related (quotient_of_relations r s) x y <-> [/\ inc x (quotient s), inc y (quotient s) & related r (rep x) (rep y)].
proof: Proof. have foq: function (fun_on_quotient s (canon_proj r)). by apply:(surj_function (foq_finer_fs fa fe)). have fc: function (canon_proj r) by fprops. have sf: source (fun_on_quotient s (canon_proj r)) = quotient s. by rewrite /fun_on_quotient/section_canon_proj; aw. move: fa =>[es er ss]. have sc:source (canon_proj r) = substrate s by aw. rewrite/quotient_of_relations; split. move /(ea_relatedP foq); rewrite sf. move => [xq yq h];split => //. have p1: (inc (rep x) (substrate r)) by rewrite ss; fprops. have p2: (inc (rep y) (substrate r)) by rewrite ss; fprops. move: h;rewrite ! foqc_V // ! canon_proj_V // => svc. by apply/(related_equiv_P er). move => [xs ys rr]; apply /(ea_relatedP foq); rewrite sf; split => //. move/(related_equiv_P er): rr => [p1 p2 p3]. by rewrite ! foqc_V // ! canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)