I am working on an exercise proof that x |-> 2 * x is continuous. the statement I write is as follows:

```
Lemma times2_continuous : continuous (fun w : R => 2%:R * w).
```

I found that there exists a theorem called `natmul_continuous`

, so I decide to prove the intermediate statement:

```
have ctn : continuous (fun w : R => w *+ 2).
exact: (@natmul_continuous _ (normedtype.numFieldNormedType.real_normedModType R))
```

I am really puzzled that I had to produce the `normedModType`

for R by hand in this unsightly manner.

I should have said that `R : realType`

in this context.

You must have the wrong import. Your example works in my setting.

```
From mathcomp Require Import matrix interval rat.
Require Import boolp reals ereal.
Require Import classical_sets posnum topology normedtype landau sequences.
Require Import derive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope ring_scope.
Lemma ctn (R : realType) : continuous (fun w : R => w *+ 2).
exact: natmul_continuous.
Qed.
```

works with me

Thansk, this solves my problem in the short term. How do you make sure to have the right sequence of imports?

I just copy and paste headers :flushed:

Where from?

from here

Thanks

This topic was moved here from #math-comp users > Using natmul_continuous on the support realType by Cyril Cohen

Last updated: Oct 13 2024 at 01:02 UTC