proposition: Lemma inc_in_setQ_sr x y: inc x y -> inc y (quotient r) -> inc x (substrate r).
proof: Proof. move=> xy /setQ_P [pa pb]; apply: (@sub_class_substrate (rep y)); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)