proposition: Lemma setID A B : A :&: B :|: A :\: B = A.
proof: Proof. by rewrite setDE -setIUr setUCr setIT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)