fact: Hypothesis (normm_s : forall k x, `|s k x| = `|k| * `|x|).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule