From 795320319c5cdf3f82ca1da475dfffbdaae4bc25 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 22 Feb 2026 17:24:02 +0900 Subject: [PATCH] fixes #1845 --- theories/normedtype_theory/pseudometric_normed_Zmodule.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 7edbaecb9e..cf93b5f978 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1105,7 +1105,9 @@ Lemma is_cvgMn f n : cvg (f @ F) -> cvg (((@GRing.natmul _)^~n \o f) @ F). Proof. by move=> /cvgMn /cvgP. Qed. Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. -Proof. by move=> ? ?; apply: continuous2_cvg => //; apply add_continuous. Qed. +Proof. +by move=> *; apply: continuous2_cvg => //; exact: (@add_continuous _ _ (a, b)). +Qed. Lemma is_cvgD f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f + g @ F). Proof. by have := cvgP _ (cvgD _ _); apply. Qed.