proposition: Lemma disjoint_setU1 A b : ~ (inc b A) -> disjoint A (singleton b).
proof: Proof. by move => pa; apply:disjoint_S; apply/set0_P=> u; case/setI2_P => /set1_P->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)