proposition: Lemma disjoint_pr1 a b: (forall x, inc x a -> inc x b -> a = b) -> (disjointVeq a b).
proof: Proof. move=> h; case: (equal_or_not a b); first by left. move=> nab;right;apply: disjoint_pr; move=> u ua ub; case: nab; apply: h ua ub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)