proposition: Lemma cosetpre_subcent1 C x : 'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].
proof: Proof. by rewrite -morphpreIdom -setIA setICA morphpreI setIS // cosetpre_cent1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)