proposition: Lemma fset1D (T : choiceType) (x:T) (A : {fset T}) : [fset x] `\` A = if x \in A then fset0 else [fset x].
proof: Proof. case: (boolP (x \in A)) => xA. - apply/eqP. by rewrite fsetD_eq0 fsub1set. - apply/fsetDidPl. by rewrite fdisjoint1X. Qed.
imports: mathcomp(all_ssreflect)