proposition: Lemma normf_div : {morph (norm : F -> F) : x y / x / y}.
proof: Proof. by move=> x y /=; rewrite normrM normfV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)