proposition: Lemma quo_rel_related_bisP x y: inc x (substrate s) -> inc y (substrate s) -> (related (quotient_of_relations r s) (class s x) (class s y) <-> related r x y).
proof: Proof. move=> xs ys. move: fa =>[es er ss]. have p1:(related r x (rep (class s x))) by apply: fe; apply: related_rep_class. have p2:(related r y (rep (class s y))) by apply: fe; apply: related_rep_class. split. move/quo_rel_relatedP=> [ixs iys rxy]. apply: (@transitivity_e _ (rep (class s x))) =>//. apply: (@transitivity_e _ (rep (class s y))) =>//. equiv_tac. move=> h; apply/quo_rel_relatedP; split; fprops. apply: (@transitivity_e _ x) =>//. apply: symmetricity_e=>//. equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)