proposition: Lemma related_equiv_P u v: related r u v <-> [/\ inc u (substrate r), inc v (substrate r) & class r u = class r v].
proof: Proof. split. by move=> ruv; split; [substr_tac | substr_tac| apply: class_eq1]. move=> [us vs cuv]. apply /class_P; rewrite cuv; by apply: inc_itself_class. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)