proposition: Lemma disjointness M: exists N, sub N M /\ ~ inc N M.
proof: Proof. set (N := Zo M (fun x => ~ (inc x x))). have NM: (sub N M) by apply: Zo_S. exists N; split => // nm. have aux: (~ (inc N N))by move=> bad; move: (bad) => /Zo_P []. by apply: (aux); apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)