proposition: Lemma setIidPl A B : reflect (A :&: B = A) (A \subset B).
proof: Proof. apply: (iffP subsetP) => [sAB | <- x /setIP[] //]. by apply/setP=> x /[1!inE]; apply/andb_idr/sAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)