proposition: Lemma setQ_P x: inc x (quotient r) <-> classp r x.
proof: Proof. apply: (iff_trans (funI_P _ _ _)); split. by move => [z zs ->]; apply: class_class. move => [pa pb]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)