proposition: Lemma genDU A B C : A \subset C -> <<C :\: A>> = <<B>> -> <<A :|: B>> = <<C>>.
proof: Proof. move=> sAC; rewrite -joingE -joing_idr => <- {B}; rewrite joing_idr. by congr <<_>>; rewrite setDE setUIr setUCr setIT; apply/setUidPr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)