proposition: Lemma valgM : {in setT &, {morph val : x y / (x : subg_of) * y >-> x * y}}.
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)