proposition: Lemma normP x A : reflect (A :^ x = A) (x \in 'N(A)).
proof: Proof. suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)