proposition: Lemma dd_pr4 F : (disjointness_degree F = \1c) <-> (~ small_set F /\ disjoint_set F).
proof: Proof. split => h. split; first by move /dd_pr3; rewrite h; fprops. move => x y xf yf; case: (equal_or_not x y); first by left. move => xny; move: (dd_pr1 xf yf xny); rewrite h. by move /clt1 /card_nonempty; right. move: h => [/dd_pr3 dn0 h1]; have /cle_eqVlt: disjointness_degree F <=c \1c. apply: (dd_pr2 CS1) => x y xF yF; case: (h1 _ _ xF yF) => // -> _. rewrite cardinal_set0 ; exact: clt_01. by case => // /clt1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)