proposition: Lemma dd_pr3 F : (disjointness_degree F = \0c) <-> small_set F.
proof: Proof. split => h. move => x y fx fy; ex_middle xy. by move: (dd_pr1 fx fy xy); rewrite h => /clt0. by apply: cle0; apply: (dd_pr2 CS0) => x y xf yf; move: (h _ _ xf yf). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)