proposition: Lemma class_dichot x y: classp r x -> classp r y -> disjointVeq x y.
proof: Proof. move=> cx cy; mdi_tac xy. move => u ux uy; case: xy. move: (rel_in_class cx ux) => pa. move: (rel_in_class cy uy) => pb. rewrite (proj2 cx) (proj2 cy); apply: class_eq1; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)