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