proposition: Lemma dd_pr2 F z: cardinalp z -> (forall x y, inc x F -> inc y F -> x <> y -> cardinal (x \cap y) <c z) -> (disjointness_degree F) <=c z.
proof: Proof. move => cz h; apply:csup_s2 => //. move=> t /funI_P [u _ ->]; fprops. move => y /funI_P [t /setC_P [/setX_P [pt Pt Qt] pb ->]]; apply: h => //. by dneg h; apply /diagonal_i_P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)