proposition: Lemma norm_gen A : 'N(A) \subset 'N(<<A>>).
proof: Proof. by apply/normsP=> x Nx; rewrite -genJ (normP Nx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)