proposition: Lemma sgvalM : {in setT &, {morph sgval : x 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)