proposition: Lemma class_P x y: inc y (class r x) <-> related r x y.
proof: Proof. have gr: (sgraph r) by fprops. rewrite /related; split. by move/funI_P => [z /Zo_P [pa <-] ->]; rewrite (gr _ pa). by move=> h; apply/funI_P; exists (J x y); [ apply: Zo_i |]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)