I'm stuck on something probably really stupid: `-->`

isn't available after `From mathcomp.analysis Require Import topology sequences`

.

My complete file is:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope ring_scope.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

This notation is in the scope `classical_set_scope`

. This can be observed by looking at its definition in `topology.v`

.

so maybe `Require Import classical_sets`

and open scope, but then you may also need `Require Import normedtype`

and `Import numFieldNormedType.Exports`

to type check the `--> +oo`

notation.

Ah, that's better, but I'm still not there yet: now `geometric 1 r`

and `+oo`

and `-->`

are recognized, but the types don't match!

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import normedtype topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope classical_set_scope.
Open Scope ring_scope.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

IIRC +oo requires realType.

What do you mean by "requires realType"? As far as I understand, that's what I have and the error message isn't about +oo but about geometric:

```
In environment
RR : realFieldType
r : RR
The term "Phantom (RR) ^nat (geometric 1 r)" has type
"phantom (sequence (GRing.Field.sort (Num.RealField.fieldType RR)))
(@geometric (Num.RealField.fieldType RR)
(GRing.one (GRing.Field.ringType (Num.RealField.fieldType RR))) r)"
while it is expected to have type "phantom (@Filtered.sort ?X ?fX) ?x".
```

I mean it should be `RR: realType`

not `RR: realFieldType`

. `realFieldType`

does not even have filteredtype struture, so you cannot use topological reasoning like `--> +oo`

.

@abab9579 Changing to `RR: realType`

means I also have to require import `reals`

, but doesn't solve the problem. I posted my whole file to show the problem ; if you have a solution, can you also post it in full?

As @Reynald Affeldt pointed out there were a few missing imports (namely`classical_sets`

and `numFieldNormedType.Exports`

) to make it work:

```
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import normedtype topology sequences.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope classical_set_scope.
Open Scope ring_scope.
Import numFieldNormedType.Exports.
Section First.
Variable RR: realFieldType.
Variable r: RR.
Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.
End First.
```

Last updated: Feb 05 2023 at 14:02 UTC