proposition: Lemma setIAC A B C : A :&: B :&: C = A :&: C :&: B.
proof: Proof. by rewrite -!setIA (setIC B). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)