proposition: Lemma satr_neqP (A B : {fset T}) : A != B -> exists x, (x \in A /\ x \notin B) \/ (x \in B /\ x \notin A).
proof: Proof. rewrite eqEsub negb_and => P. move: (orP P) => {P} [P|P]. - move: (satr_notSub A B P) => {P} [x [P Q]]. exists x; by left. - move: (satr_notSub B A P) => {P} [x [P Q]]. exists x; by right. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq choice) CompDecModal.libs(edone bcase base fset)