proposition: Lemma transitivity_e r v u w: equivalence r -> related r u v -> related r v w -> related r u w.
proof: Proof. move=> er r1 r2; apply: ((proj43 er) _ _ _ r1 r2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)