proposition: Lemma is_class_pr x y: inc x y -> inc y (quotient r) -> y = class r x.
proof: Proof. move=> xy yq. have <-: class r (rep y) = y by apply: class_rep. apply: class_eq1=>// ; apply: (related_rep_in_class yq xy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)