proposition: Lemma natmul_continuous n : continuous (fun x : V => x *+ n).
proof: Proof. case: n => [|n] x; first exact: cvg_cst. apply/cvgrPdist_lt=> _/posnumP[e]; near=> a. by rewrite -mulrnBl normrMn -mulr_natr -ltr_pdivlMr. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule