proposition: Lemma trivIsetI P D : trivIset P -> trivIset (P ::&: D).
proof: Proof. by apply: trivIsetS; rewrite -setI_powerset subsetIl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)