proposition: Lemma subsetD1 A B x : (A \subset B :\ x) = (A \subset B) && (x \notin A).
proof: Proof. by rewrite setDE subsetI subsetC sub1set inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)