proposition: Lemma in_class_relatedP y z: related r y z <-> (exists x, [/\ classp r x, inc y x & inc z x]).
proof: Proof. split. move=> ryx;exists (class r y). have ys: inc y (substrate r) by substr_tac. split; first (by apply: class_class); apply/class_P => //; equiv_tac. move =>[w [ [_ ->]]] /class_P pb /class_P pc; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)