proposition: Lemma setIDv A B : B :&: (A :\: B) = set0.
proof: Proof. apply/eqP; rewrite -subset0; apply/subsetP => x. by rewrite !inE => /and3P[->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)