Adapt to coq#19611

[Tragicus]

Motivation for this change

#1300 was merged between the last CI of rocq-prover/rocq#19611 and it being merged. It so happens that the latter PR breaks the former, so this fixes it.
N.B. I am confused that there is a TopologicalLmodule structure but nbhs0N_subproof is defined with a topologicalType with a GRing.Lmodule class. @mkerjean pointed me to #1300 (comment). Would it make sense to redefine the section in order to use TopologicalLmodule.type.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

Adapt to mc#19611

I guess it's Coq? (commit title too)

[Tragicus]

Yes, thanks.

[pi8027]

N.B. I am confused that there is a TopologicalLmodule structure but nbhs0N_subproof is defined with a topologicalType with a GRing.Lmodule class. @mkerjean pointed me to #1300 (comment). Would it make sense to redefine the section in order to use TopologicalLmodule.type.

+1

[Tragicus]

As discussed here, I changed the context in which a few lemmas are declared, along with some typing annotations.