proposition: Lemma related_rep_in_class x y: inc x (quotient r) -> inc y x -> related r (rep x) y.
proof: Proof. move=> xq; move: (xq) =>/setQ_P cx yx; apply/in_class_relatedP; exists x. split => //;by apply: setQ_repi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)