proposition: Lemma related_rr_P u v: inc u (quotient r) -> inc v (quotient r) -> (related r (rep u) (rep v) <-> (u = v)).
proof: Proof. move => uq vq; split. move=> h; rewrite - (class_rep uq) -(class_rep vq). by apply: class_eq1. by move=> ->; apply: (reflexivity_e er); apply: rep_i_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)