proposition: Lemma setU_setUD A (E F : {set A}) : E :|: F = F :|: E :\: F.
proof: Proof. apply/setP => a; rewrite !inE; apply/orP/orP => -[->|H] ; [ by rewrite andbT; apply/orP; rewrite orbN | by left | by right | case/andP : H => _ ->; by left ]. Qed.
imports: mathcomp(all_ssreflect fingroup perm)