proposition: Lemma disjoint1s (A : pred V) (x : V) : [disjoint [set x] & A] = (x \notin A).
proof: Proof. apply/pred0P/idP=> [/(_ x)/=|]; first by rewrite inE eqxx /= => ->. by move=> xNA y; rewrite !inE; case: eqP => //= ->; apply/negbTE. Qed.
imports: HB(structures) mathcomp(all_ssreflect)