diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index abfeca0128..860189dbc9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -260,6 +260,9 @@
 - in `real_interval.v`:
   + lemma `set1_bigcap_oo`
 
+- in `subspace_topology.v`:
+  + lemma `cst_within_continuous`
+
 ### Changed
 
 - in `realsum.v`:
diff --git a/theories/derive.v b/theories/derive.v
index aadc6c86c9..42d06dbe2a 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -348,7 +348,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
   by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
 rewrite /g2.
 have [->|v0] := eqVneq v 0.
-  rewrite (_ : (fun _ => _) = cst 0); last exact: cvg_cst.
+  rewrite (_ : (fun _ => _) = cst 0)//.
   by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
 apply/cvgrPdist_lt => e e0.
 rewrite nearE /=; apply/nbhs_ballP.
@@ -1372,8 +1372,8 @@ have fn0 : 0^' [set h | f (h *: v + x) != 0].
 have : (fun h => - ((f x)^-1 * (f (h *: v + x))^-1) *:
   (h^-1 *: (f (h *: v + x) - f x))) @ 0^' -->
   - (f x) ^- 2 *: 'D_v f x.
-  by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM;
-     [exact: cvg_cst|  exact: cvgV].
+  by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM => //;
+     exact: cvgV.
 apply: cvg_trans => A [_/posnumP[e] /= Ae].
 move: fn0; apply: filter_app; near=> h => /= fhvxn0.
 have he : ball 0 e%:num (h : R) by near: h; exists e%:num => /=.
@@ -2149,9 +2149,8 @@ move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
         h (shift x (k *: v)) @[k --> nbhs 0^'] --> h x.
       move=> ch.
       apply: cvg_comp; last exact: ch.
-      rewrite -[in nbhs x](add0r x).
-      apply: cvgD; last exact: cvg_cst.
-      rewrite -(scale0r v); apply: cvgZ; last exact: cvg_cst.
+      rewrite -[in nbhs x](add0r x); apply: cvgD => //.
+      rewrite -(scale0r v); apply: cvgZ => //.
       exact: nbhs_dnbhs.
     apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
     by apply: cvgB; exact: Hf.
diff --git a/theories/esum.v b/theories/esum.v
index 3dc94ddbfa..a04945c9b5 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -877,7 +877,7 @@ suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R.
   rewrite [X in  X - _]summable_nneseries_lim//; first exact/summable_funepos.
   rewrite [X in _ - X]summable_nneseries_lim//; first exact/summable_funeneg.
   rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
-    by apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB) => //; exact: cvg_cst.
+    exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB).
   apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
   by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge.
 have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R.
diff --git a/theories/ftc.v b/theories/ftc.v
index d8f7a9b55e..5fed61ad38 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -1181,11 +1181,11 @@ Lemma integration_by_substitution_oppr G a b : (a <= b)%R ->
 Proof.
 move=> ab cG; have Dopp: (@GRing.opp R)^`() = cst (-1)%R.
   by apply/funext => z; rewrite derive1E derive_val.
-rewrite (@integration_by_substitution_decreasing -%R)//.
+rewrite (@integration_by_substitution_decreasing -%R _ _ _ ab _ _ _ _ _ cG).
 - by move=> ? ? _ _; rewrite ltrN2.
-- by rewrite Dopp => ? _; exact: cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
+- by rewrite Dopp//; apply: in1W; exact: cst_continuous.
+- by rewrite Dopp.
+- by rewrite Dopp.
 - split => //.
   + by rewrite -at_leftN; exact: cvg_at_left_filter.
   + by rewrite -at_rightN; exact: cvg_at_right_filter.
@@ -1426,19 +1426,17 @@ Proof.
 move=> /continuous_within_itvNycP[cG GNa] G0.
 have Dopp : (@GRing.opp R)^`() = cst (- 1)%R.
   by apply/funext => z; rewrite derive1E derive_val.
-rewrite decreasing_ge0_integration_by_substitutiony//.
+rewrite (decreasing_ge0_integration_by_substitutiony _ _ _ _ _ _ _ G0).
 - by move=> x y _ _; rewrite ltrN2.
-- by rewrite Dopp => ? _; exact: cst_continuous.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- split.
-  + by [].
-  + by apply: cvgN; exact: cvg_at_right_filter.
-  exact/cvgNrNy.
+- by rewrite Dopp; apply: in1W; exact: cst_continuous.
+- by rewrite Dopp.
+- by rewrite Dopp.
+- by split => //; apply: cvgN; exact: cvg_at_right_filter.
+- exact/cvgNrNy.
 - exact/continuous_within_itvNycP.
-apply: eq_integral => x _; congr EFin.
-rewrite fctE -[RHS]mulr1; congr *%R.
-by rewrite fctE derive1E deriveN// opprK derive_id.
+- apply: eq_integral => x _; congr EFin.
+  rewrite fctE -[RHS]mulr1; congr *%R.
+  by rewrite fctE derive1E deriveN// opprK derive_id.
 Qed.
 
 Lemma increasing_ge0_integration_by_substitutiony F G a :
@@ -1804,11 +1802,11 @@ have dshiftE : (shift e)^`() = cst 1.
   by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutiony _ (shift e))//=.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE => ? _; exact: cst_continuous.
-- by rewrite dshiftE; exact: is_cvg_cst.
-- by rewrite dshiftE; exact: is_cvg_cst.
+- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
+- by rewrite dshiftE.
+- by rewrite dshiftE.
 - split; first by move=> x _; exact: ex_derive.
-  by apply/cvg_at_right_filter; apply: cvgD => //; exact: cvg_cst.
+  by apply/cvg_at_right_filter; exact: cvgD.
 - exact: cvg_addrr.
 by rewrite dshiftE mulr1.
 Qed.
@@ -1824,11 +1822,11 @@ have dshiftE : (shift e)^`() = cst 1.
   by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutionNy _ (shift e))//.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE => ? _; exact: cst_continuous.
-- by rewrite dshiftE; exact: is_cvg_cst.
-- by rewrite dshiftE; exact: cvg_cst.
+- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
+- by rewrite dshiftE.
+- by rewrite dshiftE.
 - split; first by move=> x _; exact: ex_derive.
-  by apply/cvg_at_left_filter; apply: cvgD => //; exact: cvg_cst.
+  by apply/cvg_at_left_filter; exact: cvgD.
 - exact: cvg_addrr_Ny.
 by rewrite dshiftE mulr1.
 Qed.
@@ -1855,16 +1853,16 @@ rewrite onemK onem1 => -> //; last 1 first.
 - by apply: eq_integral => x xr; rewrite !fctE derive1_onem opprK mulr1.
 - by rewrite lerBlDl lerDr ltW.
 - by move=> x y _ _ xy; rewrite ler_ltB.
-- by rewrite derive1_onem; move=> ? ?; exact: cvg_cst.
-- by rewrite derive1_onem; exact: is_cvg_cst.
-- by rewrite derive1_onem; exact: is_cvg_cst.
+- by rewrite derive1_onem; apply: in1W; exact: cst_continuous.
+- by rewrite derive1_onem.
+- by rewrite derive1_onem.
 split => /=.
 - by move=> x xr1; exact: derivableB.
 - apply: cvg_at_right_filter; rewrite onemK.
   apply: (@continuous_comp_cvg _ _ _ _ onem)=> //=.
-    by move=> x; apply: continuousB => //; exact: cvg_cst.
+    by move=> x; apply: continuousB => //; exact: cst_continuous.
   by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id.
-- by apply: cvg_at_left_filter; apply: cvgB => //; exact: cvg_cst.
+- by apply: cvg_at_left_filter; exact: cvgB.
 Qed.
 
 Lemma Rintegration_by_substitution_onem (G : R -> R) (r : R) :
diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v
index b453d252b8..7663cbdef4 100644
--- a/theories/gauss_integral.v
+++ b/theories/gauss_integral.v
@@ -255,14 +255,12 @@ have := @integration_by_substitution_increasing R (fun t => t * x)
 rewrite -/mu mul0r mul1r => ->//=.
 - move=> a b; rewrite !in_itv/= => /andP[a0 a1] /andP[b0 b1] ab.
     by rewrite ltr_pM2r.
-- by rewrite derM => z _; exact: cvg_cst.
-- by rewrite derM; exact: is_cvg_cst.
-- by rewrite derM; exact: is_cvg_cst.
+- by rewrite derM; apply: in1W; exact: cst_continuous.
+- by rewrite derM.
+- by rewrite derM.
 - split => //.
-  + apply: cvg_at_right_filter.
-    by apply: cvgM => //; exact: cvg_cst.
-  + apply: cvg_at_left_filter.
-    by apply: cvgM => //; exact: cvg_cst.
+  + by apply: cvg_at_right_filter; exact: cvgM.
+  + by apply: cvg_at_left_filter; exact: cvgM.
 - by apply: continuous_subspaceT; exact: continuous_gauss_fun.
 rewrite derM.
 under eq_integral do rewrite fctE/= EFinM.
@@ -300,7 +298,7 @@ rewrite fine_le//.
   by apply: continuous_in_subspaceT => z _; exact: continuous_u.
 - apply: integrable_fin_num => //=.
   apply: continuous_compact_integrable; first exact: segment_compact.
-  by apply: continuous_subspaceT => z; exact: cvg_cst.
+  exact: cst_within_continuous.
 apply: ge0_le_integral => //=.
 - by move=> y _; rewrite lee_fin u_ge0.
 - by apply/measurable_EFinP => /=; apply/measurable_funTS; exact: measurable_u.
@@ -309,9 +307,8 @@ Qed.
 
 Let cvg_integral01_u : integral01_u x @[x --> +oo] --> 0.
 Proof.
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss_fun).
+apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss_fun) => //.
 - by near=> n => /=; rewrite integral01_u_gauss_fun integral01_u_ge0.
-- exact: cvg_cst.
 - exact: cvg_gauss_fun.
 Unshelve. all: end_near. Qed.
 
@@ -342,8 +339,7 @@ have Ig2 x : 0 < x -> (integral0_gauss x) ^+ 2 = pi / 4 - integral01_u x.
 suff: pi / 4 - integral01_u x @[x --> +oo] --> pi / 4.
   apply: cvg_trans; apply: near_eq_cvg.
   by near=> x; rewrite Ig2.
-rewrite -[in X in _ --> X](subr0 (pi / 4)).
-by apply: cvgB => //; exact: cvg_cst.
+by rewrite -[in X in _ --> X](subr0 (pi / 4)); exact: cvgB.
 Unshelve. end_near. Qed.
 
 End gauss_integral_proof.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
index 0621c32874..78c7a90d4c 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -225,17 +225,16 @@ have intRf : mu.-integrable `[x - r, x + r] (EFin \o f).
   exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf).
 rewrite /= -mulrBr -fineB.
 - by rewrite integrable_fin_num.
-- rewrite integrable_fin_num// continuous_compact_integrable// => ?.
-  exact: cvg_cst.
+- rewrite integrable_fin_num// continuous_compact_integrable//.
+  exact: cst_within_continuous.
 rewrite -integralB_EFin //.
-  by apply: continuous_compact_integrable => // ?; exact: cvg_cst.
+  by apply: continuous_compact_integrable => //; exact: cst_within_continuous.
 under [fun _ => _ + _ ]eq_fun => ? do rewrite -EFinD.
 have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E).
   under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB.
-  rewrite integrableB// continuous_compact_integrable// => ?.
-  exact: cvg_cst.
-rewrite normrM ger0_norm // -fine_abse //.
-  by rewrite integrable_fin_num.
+  rewrite integrableB// continuous_compact_integrable//.
+  exact: cst_within_continuous.
+rewrite normrM ger0_norm// -fine_abse//; first by rewrite integrable_fin_num.
 suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
     (r *+ 2 * eps)%:E)%E.
   move=> intfeps; apply: le_trans.
@@ -1130,7 +1129,7 @@ apply: (sube_cvg0 _ _).1 => //.
 move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax.
 have : (mu (ball x r))^-1 *
        `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0.
-  apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //; [|exact: cvg_cst].
+  apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //.
   near=> a; rewrite mule_ge0 ?inve_ge0///= lee_pmul2l//.
     by rewrite lebesgue_measure_ball// fin_numV// eqe mulrn_eq0/= gt_eqF.
     rewrite lebesgue_measure_ball// inver mulrn_eq0/= gt_eqF// lte_fin.
@@ -1243,11 +1242,10 @@ have E_r_ n : E x n `<=` ball x (r_ x n)%:num.
 have muEr_ n : mu (ball x (r_ x n)%:num) <= C%:E * mu (E x n).
   by rewrite /C /r_ /sval/=; case: cid => -[? ?] [].
 apply: (@squeeze_cvge _ _ _ _ (cst 0) _
-  (fun n => C%:E * davg f x (r_ x n)%:num)); last 2 first.
-  exact: cvg_cst.
+    (fun n => C%:E * davg f x (r_ x n)%:num)) => //; last first.
   move/cvge_at_rightP: fx => /(_ (fun r => (r_ x r)%:num)) fx.
-  by rewrite -(mule0 C%:E); apply: cvgeM => //;
-    [exact: cvg_cst | apply: fx; split => //; exact: r_0].
+  by rewrite -(mule0 C%:E); apply: cvgeM => //; apply: fx; split => //;
+    exact: r_0.
 near=> n.
 apply/andP; split => //=.
 apply: (@le_trans _ _ ((mu (E x n))^-1 *
@@ -1289,7 +1287,7 @@ rewrite muleA lee_pmul//.
   rewrite -(@invrK _ C) -invfM lee_fin lef_pV2//.
     rewrite posrE fine_gt0// (nicely_shrinking_gt0 (hE x))//=.
     by rewrite (nicely_shrinking_lty (hE x)).
-    by rewrite posrE mulr_gt0// ?invr_gt0// fine_gt0//.
+    by rewrite posrE mulr_gt0 ?invr_gt0 ?fine_gt0.
   rewrite lter_pdivrMl // -lee_fin EFinM fineK.
     by rewrite (nicely_shrinking_fin_num (hE x)).
   by have := muEr_ n; rewrite lebesgue_measure_ball.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
index dcc3571ed2..2c69b6bf81 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
@@ -156,9 +156,8 @@ suff: `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | @[n \oo] --> 0.
    rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl.
    move: dominated_integrable => /integrableP[?]; apply: le_lt_trans.
    by apply: (le_trans _ (@le_abse_integral _ _ _ mu D f mD _)).
-apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)).
+apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)) => //.
 - by apply: nearW => n; rewrite abse_ge0//=; exact: h.
-- exact: cvg_cst.
 - exact: dominated_cvg0.
 Qed.
 
@@ -193,7 +192,7 @@ pose f' := f \_ (D `\` N); pose g' := g \_ (D `\` N).
 pose f_' := fun n => f_ n \_ (D `\` N).
 have f_f' x : D x -> f_' ^~ x @ \oo --> f' x.
   move=> Dx; rewrite /f_' /f' /restrict in_setD mem_set//=.
-  have [/= xN|/= xN] := boolP (x \in N); first exact: cvg_cst.
+  have [//=|/= xN] := boolP (x \in N).
   apply: contraPP (xN) => h; apply/negP; rewrite negbK inE; left; left.
   by apply: subN1 => /= /(_ Dx); exact: contra_not h.
 have f_g' n x : D x -> `|f_' n x| <= g' x.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index db7889adb1..1b208f92be 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -293,8 +293,8 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
     near: n; exists (truncn (M / r)).+1 => // m /= Mrm.
     by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
   - rewrite -fx0 mule0 /g -fx0.
-    under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
-    exact: cvg_cst.
+    rewrite [X in X @ _](_ : _ = cst 0)//.
+    by under eq_fun do rewrite mule0.
 rewrite (monotone_convergence mu mD mg g0 nd_g).
 under eq_fun do rewrite /g ge0_integralZl_EFin//.
 have : 0 <= \int[mu]_(x in D) f x by exact: integral_ge0.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v
index 036ecc5327..623341da55 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
 From mathcomp Require Import interval_inference archimedean finmap.
@@ -270,11 +270,10 @@ apply: norm_cvg0.
 have {}g_d1f_0 : (\int[mu]_(y in B) `|g_ n y - ('d1 f) a y|) @[n --> \oo] --> 0.
   exact/fine_cvg.
 apply: (@squeeze_cvgr _ _ _ _ (cst 0) _ _ _ _ _ g_d1f_0) => //.
-- apply/nearW => n.
-  rewrite /= normr_ge0/= le_normr_Rintegral//.
-  rewrite /comp; under eq_fun do rewrite EFinB.
-  by apply: integrableB => //; exact: intg_.
-- exact: cvg_cst.
+apply/nearW => n.
+rewrite /= normr_ge0/= le_normr_Rintegral//.
+rewrite /comp; under eq_fun do rewrite EFinB.
+by apply: integrableB => //; exact: intg_.
 Unshelve. all: end_near. Qed.
 
 Lemma differentiation_under_integral :
diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
index 9ca587ff19..39838199fc 100644
--- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v
+++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
@@ -753,9 +753,9 @@ exists (\bigcup_(i in range f) dK i); split.
   + by move=> ? ? [? ?][? ?]; split; [exact: closedU|exact: withinU_continuous].
   + move=> i _; split; first by apply: compact_closed; have [] := dkP i.
     apply: (continuous_subspaceW (dKsub i)).
-    apply: (@subspace_eq_continuous _ _ _ (fun=> i)).
+    apply: (@subspace_eq_continuous _ _ _ (cst i)).
       by rewrite /from_subspace => ? /set_mem ->.
-    by apply: continuous_subspaceT => ?; exact: cvg_cst.
+    exact: cst_continuous.
 Qed.
 
 Let measurable_almost_continuous' (f : rT -> rT) (eps : rT) :
diff --git a/theories/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v
index 8b6a8198ab..dfc735ff08 100644
--- a/theories/measure_theory/counting_measure.v
+++ b/theories/measure_theory/counting_measure.v
@@ -65,9 +65,8 @@ have [cvg_u|dvg_u] := pselect (cvg (nseries u @ \oo)).
       rewrite [X in _ `|` X](_ : _ = set0) ?setU0// bigcup0// => i [_ /negP].
       by rewrite -leqNgt => /Nu/eqP/[!cardfs_eq0]/eqP/fset_set_set0 ->.
     by rewrite /counting /= asboolT ?sumFE// -bigcup_mkord; exact: bigcup_finite.
-  rewrite -(cvg_shiftn N)/=.
-  rewrite (_ : (fun n => _) = (fun=> \sum_(i < N) counting (F i))); last first.
-    exact: cvg_cst.
+  set l := (X in _ --> X); rewrite -(cvg_shiftn N)/= -[X in _ --> X]/(nbhs l).
+  rewrite [X in X @ _](_ : _ = cst l)//.
   apply/funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
   rewrite [X in _ + X](_ : _ = 0) ?adde0; last first.
     by rewrite -{1}(subn0 N) big_mkord.
diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v
index 6399018806..329fb4b861 100644
--- a/theories/measure_theory/dirac_measure.v
+++ b/theories/measure_theory/dirac_measure.v
@@ -50,7 +50,7 @@ move=> F mF tF mUF; rewrite /dirac indicE; have [|aFn] /= := boolP (a \in _).
   rewrite big_mkord (bigID (xpred1 (Ordinal mn)))//= big_pred1_eq/= big1/=.
     by move=> j ij; rewrite indicE (negbTE (naF _ _)).
   by rewrite adde0 indicE mem_set//; exact: ballxx.
-rewrite [X in X @ \oo --> _](_ : _ = cst 0); last exact: cvg_cst.
+rewrite [X in X @ _ --> _](_ : _ = cst 0)//.
 apply/funext => n; rewrite big1// => i _; rewrite indicE; apply/eqP.
 by rewrite eqe pnatr_eq0 eqb0; apply: contra aFn => /[!inE] aFn; exists i.
 Unshelve. all: by end_near. Qed.
diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v
index 3701117264..aac951cdb9 100644
--- a/theories/measure_theory/measure_extension.v
+++ b/theories/measure_theory/measure_extension.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
@@ -199,11 +199,10 @@ Lemma le_outer_measureIC (R : realFieldType) T
 Proof.
 pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A).
 have cvg_mu : (fun n => \sum_(i < n) mu (B i)) @ \oo --> mu (B 0%N) + mu (B 1%N).
-  rewrite -2!cvg_shiftS /=.
-  rewrite [X in X @ \oo --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N))).
-    rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
-    by rewrite /B /bigcup2 /=.
-  exact: cvg_cst.
+  set l := (X in _ --> X); rewrite -2!cvg_shiftS -[X in _ --> X]/(nbhs l)/=.
+  rewrite [X in X @ _ --> _](_ : _ = cst l)//.
+  rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
+  by rewrite /B /bigcup2 /=.
 have := outer_measure_sigma_subadditive mu B.
 suff : \bigcup_n B n = X.
   move=> -> /le_trans; apply; under eq_fun do rewrite big_mkord.
@@ -637,18 +636,19 @@ Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
   measurable X -> mu^* X = mu X.
 Proof.
 move=> mX; apply/eqP; rewrite eq_le; apply/andP; split.
-  apply: ereal_inf_lbound; exists (fun n => if n is 0%N then X else set0).
-    by split=> [[]// _|t Xt]; exists 0%N.
-  apply/cvg_lim => //; rewrite -cvg_shiftS.
-  rewrite (_ : [sequence _]_n = cst (mu X)); last exact: cvg_cst.
+  set f := fun n => if n is 0%N then X else set0.
+  apply: ereal_inf_lbound; exists f.
+    by split=> [[]//=|t Xt]; exists 0%N.
+  apply/cvg_lim => //; rewrite -cvg_shiftS -[X in _ --> X]/(nbhs (mu X)).
+  rewrite [X in X @ _](_ : _ = cst (mu X))//.
   by rewrite funeqE => n /=; rewrite big_nat_recl//= big1 ?adde0.
 apply/le_ereal_inf_tmp => x [A [mA XA] <-{x}].
 have XUA : X = \bigcup_n (X `&` A n).
   rewrite predeqE => t; split => [Xt|[i _ []//]].
   by have [i _ Ait] := XA _ Xt; exists i.
 apply: (@le_trans _ _ (\sum_(i <oo) mu (X `&` A i))%E).
-  by rewrite measure_sigma_subadditive//= -?XUA => // i; apply: measurableI.
-apply: lee_lim; [exact: is_cvg_nneseries|exact: is_cvg_nneseries|].
+  by rewrite measure_sigma_subadditive//= -?XUA => // i; exact: measurableI.
+apply: lee_lim; [exact: is_cvg_nneseries..|].
 by apply: nearW => n; apply: lee_sum => i  _; exact: measureIr.
 Qed.
 
diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index ca0ce40ffa..eba1a7ccdc 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -556,7 +556,7 @@ Arguments msum {d T R}.
 
 Section measure_zero.
 Local Open Scope ereal_scope.
-Context d (T : sigmaRingType d) (R : realFieldType).
+Context {d} {T : sigmaRingType d} {R : realFieldType}.
 
 Definition mzero (A : set T) : \bar R := 0.
 
@@ -566,9 +566,8 @@ Let mzero_ge0 B : 0 <= mzero B. Proof. by []. Qed.
 
 Let mzero_sigma_additive : semi_sigma_additive mzero.
 Proof.
-move=> F mF tF mUF; rewrite [X in X @ \oo--> _](_ : _ = cst 0).
-  by apply/funext => n; rewrite big1.
-exact: cvg_cst.
+move=> F mF tF mUF; rewrite [X in X @ _ --> _](_ : _ = cst 0)//.
+by apply/funext => n; rewrite big1.
 Qed.
 
 HB.instance Definition _ := isMeasure.Build _ _ _ mzero
@@ -612,7 +611,7 @@ move=> F mF tF mUF; rewrite [X in X @ \oo --> _](_ : _ =
     (fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))).
   by apply/funext => k; rewrite ge0_sume_distrr.
 rewrite /mscale; have [->|r0] := eqVneq r%:num 0%R.
-  rewrite mul0e [X in X @ \oo --> _](_ : _ = cst 0); last exact: cvg_cst.
+  rewrite mul0e [X in X @ \oo --> _](_ : _ = cst 0)//.
   by under eq_fun do rewrite mul0e.
 by apply: cvgeZl => //; exact: measure_semi_sigma_additive.
 Qed.
@@ -1710,7 +1709,7 @@ have F0E r : mu (F 0%N) - (mu (F 0%N) - r) = r.
 rewrite -[x in _ --> x] F0E.
 have -> : mu \o F = fun n => mu (F 0%N) - (mu (F 0%N) - mu (F n)).
   by apply: funext => n; rewrite F0E.
-apply: cvgeB; rewrite ?fin_num_adde_defr//; first exact: cvg_cst.
+apply: cvgeB; rewrite ?fin_num_adde_defr//.
 have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n.
   by rewrite setIidr//; exact: bigcap_inf.
 rewrite -measureD // setDE setC_bigcap setI_bigcupr -[x in bigcup _ x]/G.
diff --git a/theories/measure_theory/signed_measure.v b/theories/measure_theory/signed_measure.v
index 9cf733b740..e9d02fee29 100644
--- a/theories/measure_theory/signed_measure.v
+++ b/theories/measure_theory/signed_measure.v
@@ -374,7 +374,7 @@ Proof. by []. Qed.
 
 Let czero_sigma_additive : semi_sigma_additive czero.
 Proof.
-move=> F mF tF mUF; rewrite [X in X @ _ --> _](_ : _ = cst 0); last exact: cvg_cst.
+move=> F mF tF mUF; rewrite [X in X @ _ --> _](_ : _ = cst 0)//.
 by apply/funext => n; rewrite big1.
 Qed.
 
@@ -416,7 +416,7 @@ move=> F mF tF mUF; rewrite /cscale; rewrite [X in X @ _ --> _](_ : _ =
   apply/funext => k; rewrite fin_num_sume_distrr// => i j _ _.
   by rewrite fin_num_adde_defl// fin_num_measure.
 rewrite /mscale; have [->|r0] := eqVneq r 0%R.
-  rewrite mul0e [X in X @ _ --> _](_ : _ = (fun=> 0)); last exact: cvg_cst.
+  rewrite mul0e [X in X @ _ --> _](_ : _ = cst 0)//.
   by under eq_fun do rewrite mul0e.
 by apply: cvgeZl => //; exact: charge_semi_sigma_additive.
 Qed.
@@ -738,10 +738,9 @@ have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
   move: cvg_nuA; rewrite -(@fineK _ (nu Aoo)) ?fin_num_measure//.
   by move=> /fine_cvgP[_ ?]; apply/cvg_ex; exists (fine (nu Aoo)).
 have mine_cvg_0 : (mine (g_ (v n) * 2^-1%:E) 1) @[n --> \oo] --> 0.
-  apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n))));
-    [|exact: cvg_cst|by []].
+  apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n)))) => //.
   by apply: nearW => n /=; rewrite nuA_g_ andbT le_min lee01 andbT mule_ge0.
-have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => //=.
+have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => /=.
 have nuDAoo : nu D >= nu (D `\` Aoo).
   rewrite -[in leRHS](@setDUK _ Aoo D).
     by apply: bigcup_sub => i _; exact: A_D.
@@ -898,8 +897,7 @@ apply: not_s_cvg_0.
 rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E).
   by apply/funext => n/=; rewrite -muleA -EFinM mulVf ?mule1.
 rewrite (_ : 0 = 0 * 2%:E); first by rewrite mul0e.
-apply: cvgeM; [by rewrite mule_def_fin| |exact: cvg_cst].
-apply/fine_cvgP; split.
+apply: cvgeM => //; apply/fine_cvgP; split.
   move/cvgrPdist_lt : maxe_cvg_0 => /(_ _ ltr01)[M _ hM]; near=> n.
   have /hM : (M <= n)%N by near: n; exists M.
   rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 80e2cc4f9d..d68d5eb3d8 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -502,12 +502,12 @@ Arguments scale_continuous _ _ : clear implicits.
 
 Lemma scaler_continuous k : continuous (fun x : V => k *: x).
 Proof.
-by move=> x; apply: (cvg_comp2 (cvg_cst _) cvg_id (scale_continuous _ _ (_, _))).
+by move=> x; exact: (cvg_comp2 _ cvg_id (scale_continuous _ _ (_, _))).
 Qed.
 
 Lemma scalel_continuous (x : V) : continuous (fun k : K => k *: x).
 Proof.
-by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (scale_continuous _ _ (_, _))).
+by move=> k; apply: (cvg_comp2 cvg_id _ (scale_continuous _ _ (_, _))).
 Qed.
 
 End NormedModule_numFieldType.
@@ -585,13 +585,13 @@ Lemma is_cvgZ s f : cvg (s @ F) ->
 Proof. by have := cvgP _ (cvgZ _ _); apply. Qed.
 
 Lemma cvgZr_tmp s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a.
-Proof. by move=> ?; apply: cvgZ => //; exact: cvg_cst. Qed.
+Proof. by move=> ?; exact: cvgZ. Qed.
 
 Lemma is_cvgZr_tmp s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F).
 Proof. by have := cvgP _ (cvgZr_tmp  _); apply. Qed.
 
 Lemma cvgZl_tmp k f a : f @ F --> a -> k \*: f @ F --> k *: a.
-Proof. by apply: cvgZ => //; exact: cvg_cst. Qed.
+Proof. exact: cvgZ. Qed.
 
 Lemma is_cvgZl_tmp k f : cvg (f @ F) -> cvg (k *: f  @ F).
 Proof. by have := cvgP _ (cvgZl_tmp  _); apply. Qed.
@@ -928,7 +928,7 @@ move=> kfin; split.
   move=> /cvgeD-/(_ (cst k) _ isT (cvg_cst _)).
   by rewrite add0e; under eq_fun => x do rewrite subeK//.
 move: k kfin => [k _ fk| |]//; rewrite -(@subee _ k%:E)//.
-by apply: cvgeB => //; exact: cvg_cst.
+exact: cvgeB.
 Qed.
 
 Lemma abse_continuous : continuous (@abse R).
@@ -968,7 +968,7 @@ move=> [s||]/=.
 - rewrite -EFinM; apply: cvg_EFin => /=.
     by apply/nbhs_EFin; near do rewrite fin_numM//.
   move=> P /= Prs; apply/nbhs_EFin=> //=.
-  by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst.
+  by apply: near_fun => //=; apply: continuousM => //=; exact: cst_continuous.
 - rewrite gt0_muley ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
   by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivrMl.
@@ -1119,8 +1119,8 @@ Lemma continuous_min (f g : T -> R^o) x :
 Proof.
 move=> ctsf ctsg.
 under [_ \min _]eq_fun => ? do rewrite minr_absE.
-apply: cvgM; [|exact: cvg_cst]; apply: cvgD; first exact: cvgD.
-by apply: cvgN; apply: cvg_norm; apply: cvgB.
+apply: cvgM => //; apply: cvgD; first exact: cvgD.
+by apply: cvgN; apply: cvg_norm; exact: cvgB.
 Qed.
 
 Lemma continuous_max (f g : T -> R^o) x :
@@ -1129,8 +1129,8 @@ Lemma continuous_max (f g : T -> R^o) x :
 Proof.
 move=> ctsf ctsg.
 under [_ \max _]eq_fun => ? do rewrite maxr_absE.
-apply: cvgM; [|exact: cvg_cst]; apply: cvgD; first exact: cvgD.
-by apply: cvg_norm; apply: cvgB.
+apply: cvgM => //; apply: cvgD; first exact: cvgD.
+by apply: cvg_norm; exact: cvgB.
 Qed.
 
 End max_cts.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 920f434388..9bacaccb3f 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -512,7 +512,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma natmul_continuous n : continuous (fun x : V => x *+ n).
 Proof.
-case: n => [|n] x; first exact: cvg_cst.
+case: n => [|n] x; first exact: cst_continuous.
 apply/cvgrPdist_lt=> _/posnumP[e]; near=> a.
 by rewrite -mulrnBl normrMn -mulr_natr -ltr_pdivlMr.
 Unshelve. all: by end_near. Qed.
@@ -1104,19 +1104,19 @@ by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply.
 Qed.
 
 Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a.
-Proof. by move=> Cfa; apply: cvg_sub0 Cfa (cvg_cst _). Qed.
+Proof. by move=> Cfa; exact: cvg_sub0 Cfa (cvg_cst _). Qed.
 
 Lemma subr_cvg0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a.
 Proof.
 split=> [?|fFk]; first exact: cvg_zero.
-by rewrite -(@subrr _ a)//; apply: cvgB => //; exact: cvg_cst.
+by rewrite -(@subrr _ a)//; exact: cvgB.
 Qed.
 
 Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K).
-Proof. by apply: continuous_cvg; apply: norm_continuous. Qed.
+Proof. by apply: continuous_cvg; exact: norm_continuous. Qed.
 
 Lemma is_cvg_norm f : cvg (f @ F) -> cvg ((Num.norm \o f : T -> K) @ F).
-Proof. by have := cvgP _ (cvg_norm _); apply. Qed.
+Proof. by have := cvgP _ (cvg_norm _); exact. Qed.
 
 Lemma norm_cvg0P f : `|f x| @[x --> F] --> (0:K^o) <-> f @ F --> 0.
 Proof.
diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v
index 7378548295..370392ff28 100644
--- a/theories/normedtype_theory/urysohn.v
+++ b/theories/normedtype_theory/urysohn.v
@@ -319,7 +319,7 @@ have [eps exy] : exists (eps : {posnum R}),
   move=> x y Ax By bxy; have divxy := epsdiv (x, y) bxy.
   by have : set0 (x, y) by rewrite -AB0; split.
 have [->|/set0P[a A0]] := eqVneq A set0.
-  exists (fun=> 1); split; first by move => ?; exact: cvg_cst.
+  exists (cst 1); split; first exact: cst_continuous.
   - by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
   - by rewrite image_set0.
   - by move=> ? [? ? <-].
@@ -330,12 +330,12 @@ have dfin x : @edist_inf R T' A x \is a fin_num.
   exact: countable_uniform.countable_uniform_bounded.
 pose f' := (fun z => fine (@edist_inf R T' A z)) \min (fun=> eps%:num).
 pose f z := (f' z)/eps%:num; exists f; split.
-- move=> x; rewrite /f; apply: (@cvgM R T (nbhs x)); last exact: cvg_cst.
+- move=> x; rewrite /f; apply: (@cvgM R T (nbhs x)) => //.
   suff : {for x, continuous (f' : T' -> R)}.
     move=> Q U; rewrite nbhs_simpl /= => f'U.
     have [J /(gauge.gauge_ent entE) entJ/filterS] := Q _ f'U; apply.
     by rewrite nbhs_simpl /= -nbhs_entourageE /=; exists J.
-  apply: continuous_min; last by apply: cvg_cst; exact: nbhs_filter.
+  apply: continuous_min; last exact: cst_continuous.
   apply: fine_cvg; first exact: nbhs_filter.
   rewrite fineK //; first exact: edist_inf_continuous.
 - move=> _ [x _ <-]; rewrite set_itvE /=; apply/andP; split.
@@ -366,9 +366,9 @@ Local Lemma Urysohn' (A B : set T) : exists (f : T -> R),
 Proof.
 have [[? [E [entE ABE0 coarseT]]]|nP] := pselect (uniform_separator A B).
   have [f] := @urysohn_separation _ R _ _ _ entE ABE0.
-  by case=> ctsf ? ? ?; exists f; split => // ? ? /= ?; apply/coarseT/ctsf.
-exists (fun=>1); split => //; first by move=> ?; exact: cvg_cst.
-by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
+  by case=> ctsf ? ? ?; exists f; split => // ? ? /= ?; exact/coarseT/ctsf.
+exists (cst 1); split => //; first exact: cst_continuous.
+by move=> ? [? _ <-]/=; rewrite bound_itvE.
 Qed.
 
 Definition Urysohn (A B : set T) : T -> R := projT1 (cid (Urysohn' A B)).
diff --git a/theories/numfun.v b/theories/numfun.v
index dc674e8526..75de0d05ee 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -1272,9 +1272,9 @@ have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext R _ _ cA cB A0.
 pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=.
   move=> t; apply: continuous_comp; first exact: cf.
   apply: (@continuousD R R^o).
-    apply: continuousM; last exact: cvg_cst.
-    by apply: (@continuousB R R^o) => //; exact: cvg_cst.
-  by apply: continuousM; [exact: cvg_id|exact: cvg_cst].
+    apply: continuousM; last exact: cst_continuous.
+    by apply: (@continuousB _ R^o) => //; exact: cst_continuous.
+  by apply: continuousM => //; exact: cst_continuous.
 - by rewrite -image_comp => z /= [? /f0 -> <-]; rewrite line_path0.
 - by rewrite -image_comp => z /= [? /f1 -> <-]; rewrite line_path1.
 - rewrite -image_comp; apply: (subset_trans (image_subset _ f01)).
@@ -1398,7 +1398,7 @@ exists (lim (h_ @ \oo)); split.
   by rewrite (le_trans ((f_geo n).2 _ _)) // ler_norm.
 - apply: (@uniform_limit_continuous X _ (h_ @ \oo) (lim (h_ @ \oo))) =>//.
   near_simpl; apply: nearW; elim.
-    by rewrite /h_ /series /= big_geq// => ?; exact: cvg_cst.
+    by rewrite /h_ /series /= big_geq// => ?; exact: cst_continuous.
   move=> n; rewrite /h_ /series /= big_nat_recr /= // => IH t.
   by apply: continuousD; [exact: IH|exact: g_cts].
 - move=> t.
diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v
index 826419ef21..cba5fe4120 100644
--- a/theories/pi_irrational.v
+++ b/theories/pi_irrational.v
@@ -368,7 +368,7 @@ apply: (@le_lt_trans _ _
     (\int[mu]_(x in `[0, pi]) (pi ^+ n * a ^+ n / n`!%:R))).
   apply: le_Rintegral => //=.
   - apply/continuous_compact_integrable; first exact: segment_compact.
-    by apply/continuous_subspaceT => x; exact: cvg_cst.
+    exact: cst_within_continuous.
   - move=> x.
     have ? : 0 <= pi ^+ n * a ^+ n / n`!%:R :> R.
       by rewrite mulr_ge0// mulr_ge0// exprn_ge0// pi_ge0.
@@ -403,7 +403,7 @@ move/rationalP => [a [b]]; have [->|b0 piratE] := eqVneq b O.
   by rewrite invr0 mulr0; apply/eqP; rewrite gt_eqF// pi_gt0.
 have [na ana] : exists na, (a%:~R = na%:R :> R)%R.
   exists `|a|%N; rewrite natr_absz gtr0_norm//.
-  by have := @pi_gt0 R; rewrite piratE pmulr_lgt0 ?invr_gt0 ?ltr0n ?lt0n// ltr0z.
+  by have := @pi_gt0 R; rewrite piratE pmulr_lgt0 ?invr_gt0 ?ltr0n ?lt0n ?ltr0z.
 rewrite {}ana in piratE.
 have [N _] := pi_irrational.intfsin_small b0 (esym piratE) (@ltr01 R).
 near \oo%classic => n.
diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index 93e8e85af6..4db8a20854 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -48,7 +48,7 @@ Implicit Types x y : R.
 Lemma continuous_onemXn n x : {for x, continuous (fun y => y.~ ^+ n)}.
 Proof.
 apply: (@continuous_comp _ _ _ (@onem R) (fun x => x ^+ n)).
-  by apply: (@cvgB _ R^o); [exact: cvg_cst|exact: cvg_id].
+  exact: (@cvgB _ R^o).
 exact: exprn_continuous.
 Qed.
 
@@ -65,11 +65,11 @@ Lemma derivable_oo_LRcontinuous_onemXnMr n x :
 Proof.
 split.
 - by move=> y y01; apply: derivableM => //=; exact: onemXn_derivable.
-- apply: cvgM; last exact: cvg_cst.
+- apply: cvgM => //.
   apply: cvg_at_right_filter; apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
     by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
   exact: exprn_continuous.
-- apply: cvg_at_left_filter; apply: cvgM; last exact: cvg_cst.
+- apply: cvg_at_left_filter; apply: cvgM => //.
   apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
     by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
   exact: exprn_continuous.
@@ -264,7 +264,7 @@ rewrite (@Rintegration_by_parts _ _ (fun x => x.~ ^+ b.+1 / - b.+1%:R)
     (fun x => a.+1%:R * x ^+ a)).
 - exact: ltr01.
 - apply/continuous_subspaceT => x.
-  by apply: cvgM; [exact: cvg_cst|exact: exprn_continuous].
+  by apply: cvgM => //; exact: exprn_continuous.
 - split.
     by move=> x x01; exact: exprn_derivable.
     exact/cvg_at_right_filter/exprn_continuous.
diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v
index 9e902791a9..bbbe300f3f 100644
--- a/theories/probability_theory/normal_distribution.v
+++ b/theories/probability_theory/normal_distribution.v
@@ -116,12 +116,12 @@ Proof. by apply: measurable_funM => //=; exact: measurable_normal_fun. Qed.
 
 Lemma continuous_normal_pdf0 m s : continuous (normal_pdf0 m s).
 Proof.
-move=> x; apply: cvgM; first exact: cvg_cst.
+move=> x; apply: cvgM => //.
 apply: (cvg_comp _ expR); last exact: continuous_expR.
-apply: cvgM; last exact: cvg_cst.
-apply: (@cvgN _ R^o).
+apply: cvgM => //.
+apply: cvgN.
 apply: (cvg_comp (fun x => x - m) (fun x => x ^+ 2)).
-  by apply: (@cvgB _ R^o) => //; [exact: cvg_id|exact: cvg_cst].
+  by apply: cvgB => //; exact: cvg_id.
 exact: sqr_continuous.
 Qed.
 
@@ -248,9 +248,9 @@ congr *%E; last by rewrite -(mulr_natr (_ ^+ 2)) sqrtrM ?sqr_ge0.
 rewrite -increasing_ge0_integration_by_substitutionT//.
 - move=> x y xy; rewrite /F ltr_pM2r ?ltr_leB ?gt_eqF//.
   by rewrite invr_gt0 ?sqrtr_gt0 ?pmulrn_lgt0 ?exprn_even_gt0.
-- by rewrite F'E => ?; exact: cvg_cst.
-- by rewrite F'E; exact: is_cvg_cst.
-- by rewrite F'E; exact: is_cvg_cst.
+- by rewrite F'E; exact: cst_continuous.
+- by rewrite F'E.
+- by rewrite F'E.
 - apply/gt0_cvgMlNy; last exact: cvg_addrr_Ny.
   by rewrite invr_gt0// sqrtr_gt0 -mulr_natr mulr_gt0// exprn_even_gt0.
 - apply/gt0_cvgMly; last exact: cvg_addrr.
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 99dbb9f7b4..d3122347e5 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -331,7 +331,7 @@ have cdf_s : cdf X r @[r --> a^'+] --> s%:E.
   by exists (a + 1)%R => //; rewrite in_itv /=; apply/andP; rewrite ltrDl.
 have cdf_ns : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> s%:E.
   move/cvge_at_rightP : cdf_s; apply; split=> [n|]; rewrite ?ltrDl //.
-  rewrite -[X in _ --> X]addr0; apply: (@cvgD _ R^o); first exact: cvg_cst.
+  rewrite -[X in _ --> X]addr0; apply: cvgD => //.
   by rewrite gtr0_cvgV0 ?cvg_shiftS; [near=> n | exact: cvgr_idn].
 have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
   pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R].
@@ -372,7 +372,7 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E.
     rewrite /lsf /lebesgue_stieltjes_measure /measure_extension/=.
     rewrite measurable_mu_extE/= ?wlength_itv_bnd//; first exact: is_ocitv.
     by rewrite lerNl; near: n; exact: nbhs_infty_ger.
-  rewrite -[X in _ --> X](sube0 (f r)%:E); apply: (cvgeB _ (cvg_cst _ )) => //.
+  rewrite -[X in _ --> X](sube0 (f r)%:E); apply: cvgeB => //.
   apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy f))) => //.
   by apply: (cvg_comp _ _ cvgr_idn); rewrite ninfty.
 have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic).
@@ -479,14 +479,14 @@ Qed.
 Lemma cvg_ccdfy0 : ccdf X @ +oo%R --> 0.
 Proof.
 have : 1 - cdf X r @[r --> +oo%R] --> 1 - 1.
-  by apply: cvgeB; [| exact: cvg_cst | exact: cvg_cdfy1].
+  by apply: cvgeB => //; exact: cvg_cdfy1.
 by rewrite subee// (eq_cvg _ _ ccdf_1_cdf).
 Qed.
 
 Lemma cvg_ccdfNy1 : ccdf X @ -oo%R --> 1.
 Proof.
 have : 1 - cdf X r @[r --> -oo%R] --> 1 - 0.
-  by apply: cvgeB; [| exact: cvg_cst | exact: cvg_cdfNy0].
+  by apply: cvgeB => //; exact: cvg_cdfNy0.
 by rewrite sube0 (eq_cvg _ _ ccdf_1_cdf).
 Qed.
 
@@ -494,7 +494,7 @@ Lemma ccdf_right_continuous : right_continuous (ccdf X).
 Proof.
 move=> r.
 have : 1 - cdf X s @[s --> r^'+] --> 1 - cdf X r.
-  by apply: cvgeB; [| exact: cvg_cst | exact: cdf_right_continuous].
+  by apply: cvgeB => //; exact: cdf_right_continuous.
 by rewrite ccdf_1_cdf (eq_cvg _ _ ccdf_1_cdf).
 Qed.
 
diff --git a/theories/realfun.v b/theories/realfun.v
index 864428b846..3aec286fca 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -500,7 +500,7 @@ have [lpoo|lpoo] := eqVneq l +oo.
   by move=> m /= nm; rewrite (le_trans (ltW Mun))// ndf// ltW.
 have [fnoo|fnoo] := pselect (f = cst -oo).
   rewrite /l (_ : S = [set -oo]); last first.
-    by rewrite ereal_sup1 fnoo; exact: cvg_cst.
+    by rewrite ereal_sup1 fnoo.
   apply/seteqP; split => [_ [n _] <- /[!fnoo]//|_ ->].
   by rewrite /S fnoo; exists 0%R.
 have [/ereal_sup_ninfty lnoo|lnoo] := eqVneq l -oo.
@@ -2283,8 +2283,8 @@ have bx : - b <= - x by rewrite lerNl opprK.
 have xa : - x < - a by rewrite ltrNl opprK.
 have ? : - x <= - a by exact: ltW.
 have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter.
-have -> : fine (TV (-x) (-a) (f \o -%R)) =
-    fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)).
+have -> : fine (TV (- x) (- a) (f \o -%R)) =
+    fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) (- x) (f \o -%R)).
   apply/eqP; rewrite -subr_eq opprK addrC.
   rewrite -fineD.
     by apply/bounded_variationP => //; exact: bounded_variationl bvNf.
@@ -2293,10 +2293,10 @@ have -> : fine (TV (-x) (-a) (f \o -%R)) =
 suff /near_eq_cvg/cvg_trans : {near (- x)^'+,
     (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1
     (fine \o (TV a)^~ f) \o -%R}.
-  apply; apply: cvgB; first exact: cvg_cst.
+  apply; apply: cvgB => //.
   apply: (total_variation_right_continuous _ _ _ bvNf).
-  - by rewrite lerNl opprK //.
-  - by rewrite ltrNl opprK //.
+  - by rewrite lerNl opprK.
+  - by rewrite ltrNl opprK.
   by apply/cvg_at_leftNP; rewrite /= opprK.
 apply: filter_app (nbhs_right_lt xa).
 apply: (filter_app _ _ (nbhs_right_ge _)).
@@ -2632,7 +2632,7 @@ have hder x : x \in `]a, b[%R -> derivable h x 1.
   by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)).
 have ch : {within `[a, b], continuous h}.
   rewrite continuous_subspace_in => x xab.
-  by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]].
+  by apply: cvgB; [exact: cf|apply: cvgM => //; exact: cg].
 have /(Rolle ab hder ch)[x xab derh] : h a = h b.
   rewrite /h; apply/eqP; rewrite -subr_eq0 opprD addrACA -opprD subr_eq0.
   by rewrite -mulrBr -mulrNN -mulNr 2!opprB divfK// differentiable_subr_neq0.
@@ -2723,7 +2723,7 @@ have f0g0 y : a < y -> y < b ->
     (f0 x - f0 y) / (g0 x - g0 y) @[x --> a^'+] --> f0 y / g0 y.
   move=> ay yb; rewrite -[X in _ --> X]opprK -mulrN -invrN -mulNr.
   apply: cvgM.
-    rewrite -[X in _ --> X]add0r; apply: cvgB; last exact: cvg_cst.
+    rewrite -[X in _ --> X]add0r; apply: cvgB => //.
     apply: cvg_trans fa0; apply: near_eq_cvg; near=> z.
     by rewrite /f0 gt_eqF.
   apply: cvgV.
@@ -2736,7 +2736,7 @@ have f0g0 y : a < y -> y < b ->
     rewrite mulf_eq0// orbC gt_eqF ?subr_gt0//= => /eqP; apply/eqP.
     apply: cdg.
     by move: c0 c0ay; apply: subset_itvSoo; rewrite bnd_simp// ltW.
-  rewrite -[X in _ --> X]add0r; apply: cvgB; last exact: cvg_cst.
+  rewrite -[X in _ --> X]add0r; apply: cvgB => //.
   apply: cvg_trans ga0; apply: near_eq_cvg; near=> z.
   by rewrite /g0 gt_eqF.
 have lfg_ub q : l < q ->
diff --git a/theories/sequences.v b/theories/sequences.v
index 03a62103c1..52fce143cc 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -566,7 +566,7 @@ Proof.
 suff -> : (fun n => \sum_(N <= k < n) u_ k) =
           fun n => if (n <= N)%N then \sum_(N <= k < n) u_ k
                    else series u_ n - \sum_(0 <= k < N) u_ k.
-  by rewrite is_cvg_restrict/= is_cvgDlE//; apply: is_cvg_cst.
+  by rewrite is_cvg_restrict/= is_cvgDlE.
 rewrite funeqE => n; case: leqP => // ltNn; apply: (canRL (addrK _)).
 by rewrite seriesEnat addrC -big_cat_nat// ltnW.
 Qed.
@@ -890,10 +890,9 @@ Unshelve. all: by end_near. Qed.
 Lemma cvg_expr (R : archiRealFieldType) (z : R) :
   `|z| < 1 -> (GRing.exp z : R ^nat) @ \oo --> 0.
 Proof.
-move=> Nz_lt1; apply/norm_cvg0P; pose t := (1 - `|z|).
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)); last 2 first.
-- exact: cvg_cst.
-- by rewrite -(scaler0 _ t^-1); exact: (cvgZl_tmp cvg_harmonic).
+move=> Nz_lt1; apply/norm_cvg0P; pose t := 1 - `|z|.
+apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)) => //; last first.
+  by rewrite -(scaler0 _ t^-1); exact: (cvgZl_tmp cvg_harmonic).
 near=> n; rewrite normr_ge0 normrX/= ler_pdivlMl ?subr_gt0//.
 rewrite -(@ler_pM2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl.
 have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n.
@@ -919,8 +918,7 @@ Lemma cvg_geometric_series (R : archiRealFieldType) (a z : R) : `|z| < 1 ->
 Proof.
 move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//.
 have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1.
-by apply: cvgMr_tmp; apply: cvgMl_tmp; apply: cvgB;
-  [apply: cvg_cst|apply: cvg_expr].
+by apply: cvgMr_tmp; apply: cvgMl_tmp; apply: cvgB => //; exact: cvg_expr.
 Qed.
 
 Lemma cvg_geometric_series_half (R : archiRealFieldType) (r : R) n :
@@ -1173,7 +1171,7 @@ Proof.
 move=> u_nd [l ul].
 suff [N Nu] : exists N, forall n, (n >= N)%N -> u_ n = u_ N.
   apply/cvg_ex; exists (u_ N); rewrite -(cvg_shiftn N).
-  rewrite [X in X @ \oo --> _](_ : _ = cst (u_ N))//; last exact: cvg_cst.
+  rewrite [X in X @ \oo --> _](_ : _ = cst (u_ N))//.
   by apply/funext => n /=; rewrite Nu// leq_addl.
 apply/not_existsP => hu.
 have {hu}/choice[f Hf] : forall x, (exists n, x <= n /\ u_ n > u_ x)%N.
@@ -1233,12 +1231,12 @@ Lemma ereal_inf_seq S : S != set0 ->
 Proof.
 move=> SN0; apply/cid2; have [|Ninfy] := eqVneq (ereal_inf S) +oo.
   move=> /[dup]/ereal_inf_pinfty/subset_set1/orW[/eqP/negPn/[!SN0]//|->] ->.
-  by exists (fun=> +oo) => //; apply: cvg_cst.
+  by exists (fun=> +oo).
 suff: exists2 v : (\bar R)^nat, v @ \oo --> ereal_inf S &
         forall n, exists2 x : \bar R, x \in S & x < v n.
   move=> [v vcvg] /(_ _)/sig2W-/all_sig/= [u /all_and2[/(_ _)/set_mem Su u_lt]].
   exists u => //; move: vcvg.
-  have: cst (ereal_inf S) @ \oo --> ereal_inf S by exact: cvg_cst.
+  have: cst (ereal_inf S) @ \oo --> ereal_inf S by [].
   apply: squeeze_cvge; apply: nearW => n; rewrite /cst/=.
   by rewrite ge_ereal_inf /= 1?ltW; first by exists (u n).
 have [infNy|NinfNy] := eqVneq (ereal_inf S) -oo.
@@ -1379,11 +1377,10 @@ have [Spoo|Spoo] := pselect (S +oo).
     by move: (nd_u_ _ _ Nn); rewrite uNoo leye_eq => /eqP.
   have -> : l = +oo by rewrite /l /ereal_sup; exact: supremum_pinfty.
   rewrite -(cvg_shiftn N); set f := (X in X @ \oo --> _).
-  rewrite (_ : f = cst +oo); last exact: cvg_cst.
+  rewrite (_ : f = cst +oo)//.
   by rewrite funeqE => n; rewrite /f /= Nu // leq_addl.
 have [/funext Snoo|Snoo] := pselect (forall n, u_ n = -oo).
-  rewrite /l (_ : S = [set -oo]); last first.
-    by rewrite ereal_sup1 Snoo; exact: cvg_cst.
+  rewrite /l (_ : S = [set -oo]); last by rewrite ereal_sup1 Snoo.
   apply/seteqP; split => [_ [n _] <- /[!Snoo]//|_ ->].
   by rewrite /S Snoo; exists 0%N.
 have [/ereal_sup_ninfty loo|lnoo] := eqVneq l -oo.
@@ -1523,10 +1520,9 @@ transitivity
     (ereal_sup (range (fun m => \sum_(n <= k < m) ((f k.+1)%:E - (f k)%:E)%E))).
   by apply/cvg_lim => //; exact: ereal_nondecreasing_cvgn.
 transitivity (limn ((EFin \o f) \- cst (f n)%:E)); last first.
-  apply/cvg_lim => //; apply: cvgeB.
+  apply/cvg_lim => //; apply: cvgeB => //.
   - exact: fin_num_adde_defl.
   - by apply: ereal_nondecreasing_is_cvgn => x y xy; rewrite lee_fin ndf.
-  - exact: cvg_cst.
 have := @ereal_nondecreasing_cvgn _ _ nd_sumf.
 rewrite -(cvg_restrict n (EFin \o f \- cst (f n)%:E)) => /cvg_lim <-//.
 apply: congr_lim; apply/funext => k/=.
@@ -1585,11 +1581,9 @@ Lemma eseries0 N P : (forall i, (N <= i)%N -> P i -> f i = 0) ->
   \sum_(N <= i <oo | P i) f i = 0.
 Proof.
 move=> f0; apply/cvg_lim => //.
-under eq_fun.
-  move=> n.
-  rewrite big_nat_cond big1; first by move=> k /andP[/andP[+ _]]; exact: f0.
-  over.
-exact: cvg_cst.
+rewrite [X in X @ _](_ : _ = cst 0)//.
+apply/funext => n.
+by rewrite big_nat_cond big1; first by move=> k /andP[/andP[+ _]]; exact: f0.
 Qed.
 
 Lemma eseries_pred0 P : P =1 xpred0 -> \sum_(i <oo | P i) f i = 0.
@@ -1766,8 +1760,7 @@ Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) :
     cvgn u -> (forall n, 0 <= u n) -> -oo < l ->
   limn (fun x => l + u x) = l + limn u.
 Proof.
-move=> cu u0 hl; apply/cvg_lim => //; apply: cvgeD (cu); last first.
-  exact: cvg_cst.
+move=> cu u0 hl; apply/cvg_lim => //; apply: cvgeD (cu) => //.
 rewrite ltninfty_adde_def// inE (@lt_le_trans _ _ 0)//.
 by apply: lime_ge => //; exact: nearW.
 Qed.
@@ -2517,16 +2510,16 @@ End limn_esup_einf.
 
 Section lim_esup_inf.
 Local Open Scope ereal_scope.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types (u v : (\bar R)^nat) (l : \bar R).
 
 Lemma limn_einf_shift u l : l \is a fin_num ->
   limn_einf (fun x => l + u x) = l + limn_einf u.
 Proof.
-move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //; apply: cvg_trans; last first.
-  apply: (@cvgeD _ \oo _ _ (cst l) (einfs u) _ (limn (einfs u))).
+move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //.
+apply: cvg_trans; last first.
+  apply: (@cvgeD _ \oo _ _ (cst l) (einfs u) _ (limn (einfs u))) => //.
   - by rewrite fin_num_adde_defr.
-  - exact: cvg_cst.
   - exact: is_cvg_einfs.
 suff : einfs (fun n => l + u n) = (fun n => l + einfs u n) by move=> ->.
 rewrite funeqE => n.
@@ -2544,7 +2537,7 @@ Proof.
 move=> supul ul; have usupu n : l <= u n <= esups u n.
   by rewrite ul /=; apply/ereal_sup_ubound; exists n => /=.
 suff : esups u @ \oo --> l.
-  by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; [exact: nearW|exact: cvg_cst].
+  by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; exact: nearW.
 apply/cvg_closeP; split; first exact: is_cvg_esups.
 rewrite closeE//; apply/eqP.
 rewrite eq_le -[X in X <= _ <= _]limn_esup_lim supul/=.
@@ -3005,7 +2998,7 @@ Proof.
 move=> /finite_range_cst_subsequence[x [A Aoo Ax_]].
 have /= [|f [fincr _ Af]] := infinite_increasing_seq_wf _ Aoo 0.
   by move=> n; apply: sub_finite_set (finite_II n.+1) => m /=.
-exists f => //=; suff -> : x_ \o f = fun=> x by apply: is_cvg_cst.
+exists f => //=; suff -> : x_ \o f = fun=> x by [].
 by apply/funext => k /=; rewrite (Ax_ _).1.
 Qed.
 
diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index 8c82e106d0..84a4634400 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -1435,8 +1435,7 @@ Lemma continuous_curry (f : U * V -> W) :
     continuous (curry f) /\ forall u, continuous (curry f u).
 Proof.
 move=> ctsf; split; first last.
-  move=> u z; apply: (continuous_comp _ (ctsf (u, z))).
-  by apply: cvg_pair => //=; exact: cvg_cst.
+  by move=> u z; apply: (continuous_comp _ (ctsf (u, z))); exact: cvg_pair.
 move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO.
 near=> z => w /= [+ + <-]; near: z.
 move/compact_near_coveringP/near_covering_withinP : cptK; apply.
@@ -1579,9 +1578,8 @@ Lemma cvg_big {T : Type} (F : set_system T) (r : seq I)
 Proof.
 move=> FF cvg_f.
 elim: r => [|i r IHr].
-  rewrite big_nil.
-  under eq_cvg do rewrite big_nil.
-  exact: cvg_cst.
+  rewrite big_nil [X in X @ _](_ : _ = cst x0)//.
+  by apply/funext => t; rewrite big_nil.
 rewrite big_cons.
 under eq_cvg do rewrite big_cons.
 case: ifPn => // Pi.
diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v
index 5965dcb7a8..3039e3ce96 100644
--- a/theories/topology_theory/separation_axioms.v
+++ b/theories/topology_theory/separation_axioms.v
@@ -404,15 +404,14 @@ Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
    (\forall x \near F, f x = l) -> lim (f @ F) = l.
 Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
 
-Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
-   lim ((fun _ : U => k) @ F) = k.
-Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
+Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) : lim (@cst U _ k @ F) = k.
+Proof. exact: cvg_lim. Qed.
 
 Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
   F (fun x : U => is_subset1 (f x)) ->
   f `@ F --> l -> lim (f `@ F) = l.
 Proof.
-move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
+by move=> f_prop fl; apply: get_unique =>// l' fl'; exact: cvgi_unique _ fl' fl.
 Qed.
 
 End hausdorff_ptopologicalType.
diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index ef6d7a6e39..10bd0a0b6a 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -373,6 +373,9 @@ move=> ctsf; rewrite continuous_subspace_in => ? ?.
 exact: continuous_in_subspaceT.
 Qed.
 
+Lemma cst_within_continuous {U} A u : {within A, continuous (@cst T U u)}.
+Proof. by apply: continuous_subspaceT; exact: cst_continuous. Qed.
+
 Lemma continuous_open_subspace {U} A (f : T -> U) :
   open A -> {within A, continuous f} = {in A, continuous f}.
 Proof.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index a6170e44b1..d397a26796 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -348,18 +348,19 @@ Lemma cvg_cst (U : topologicalType) (x : U) (T : Type)
   (fun _ : T => x) @ F --> x.
 Proof. by apply: cvg_near_cst; near=> x0. Unshelve. all: by end_near. Qed.
 Arguments cvg_cst {U} x {T F FF}.
-#[global] Hint Resolve cvg_cst : core.
+#[global] Hint Extern 0 (_ @ _ --> _) => solve [apply: cvg_cst] : core.
 
 Lemma is_cvg_cst (U : ptopologicalType) (x : U) (T : Type)
   (F : set_system T) {FF : Filter F} :
   cvg ((fun _ : T => x) @ F).
-Proof. by apply: cvgP; apply: cvg_cst. Qed.
+Proof. exact: cvgP (cvg_cst _). Qed.
 Arguments is_cvg_cst {U} x {T F FF}.
-#[global] Hint Resolve is_cvg_cst : core.
+#[global] Hint Extern 0 (cvg (_ @ _)) => solve [apply: is_cvg_cst] : core.
+#[global] Hint Extern 0 (cvgn (_ @ _)) => solve [apply: is_cvg_cst] : core.
 
 Lemma cst_continuous {T U : topologicalType} (x : U) :
   continuous (fun _ : T => x).
-Proof. by move=> t; apply: cvg_cst. Qed.
+Proof. by move=> t; exact: cvg_cst. Qed.
 
 Section within_topologicalType.
 Context {T : topologicalType} (A : set T).
@@ -1084,7 +1085,7 @@ Section continuous_const.
 Context {X Y : topologicalType} (y : Y).
 
 #[local] Lemma cts_const : continuous (@cst X Y y).
-Proof. by move=> ?; exact: cvg_cst. Qed.
+Proof. by move=> x; exact: cvg_cst. Qed.
 
 HB.instance Definition _ := @isContinuous.Build X Y (cst y) cts_const.
 
diff --git a/theories/trigo.v b/theories/trigo.v
index e8da5963e3..8d65b797b9 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -1117,7 +1117,7 @@ Canonical oneDsqr_inum x : {itv R & `[1, +oo[} := @ItvReal R (oneDsqr x)
 Lemma oneDsqrV_le1 x : (oneDsqr\^-1) x <= 1. Proof. by rewrite invf_le1. Qed.
 
 Lemma continuous_oneDsqr : continuous oneDsqr.
-Proof. by move=> x; apply: cvgD; [exact: cvg_cst|exact: exprn_continuous]. Qed.
+Proof. by move=> x; apply: cvgD => //; exact: exprn_continuous. Qed.
 
 Lemma continuous_oneDsqrV : continuous (oneDsqr\^-1).
 Proof. by move=> x; apply: cvgV => //; exact: continuous_oneDsqr. Qed.