proposition: Lemma norm1 : 'N(1) = setT :> {set gT}.
proof: Proof. by apply/setP=> x; rewrite !inE conjs1g subxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)