proposition: Lemma disjoints1 (T: finType) (A : pred T) (x : T) : [disjoint A & [set x]] = (x \notin A).
proof: Proof. by rewrite disjoint_sym disjoint1s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin