proposition: Lemma add_continuous : continuous (fun z : V * V => z.1 + z.2).
proof: Proof. move=> [/= x y]; apply/cvgrPdist_lt=> _/posnumP[e]; near=> a b => /=. by rewrite opprD addrACA normm_lt_split. 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