proposition: Lemma setUUl A B C : A :|: B :|: C = (A :|: C) :|: (B :|: C).
proof: Proof. by rewrite setUA !(setUAC _ C) -(setUA _ C) setUid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)