Add support for latest version of math-comp algebra and analysis

[lyonel2017]

The changes in this PR allow to compile SSProve with the latest version of math-comp algebra and analysis.

Should solve #89 (comment)

Checklist

• update .opam, .yml, .nix file

[MarkusKL]

These changes look fine to me and it compiles locally. Thanks for doing the work.

Will @spitters or @4ever2 start the pipeline? The extra required manual step looks new to me. Ping #89.

🎉

ROCQ compile theories/Crypt/Main.v
Axioms:
boolp.propositional_extensionality : ∀ P Q : Prop, P ↔ Q → P = Q
boolp.functional_extensionality_dep :
  ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
    (∀ x : A, f x = g x) → f = g
FunctionalExtensionality.functional_extensionality_dep :
  ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
    (∀ x : A, f x = g x) → f = g
boolp.constructive_indefinite_description :
  ∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}
SPropBase.ax_proof_irrel : ClassicalFacts.proof_irrelevance
Axioms.R : reals.Real.type

[4ever2]

The Nix CI fails because the branch is from a fork. Feel free to merge if opam and flake workflows succeed.

[remix7531]

I built this PR from source against MathComp 2.6.0 and mathcomp-analysis 1.17.0: it compiles and the admitted sum interchange lemma disappears.

Two notes:

• The failing opam workflow is caused by its own pins, which install a MathComp too old for the renamings this PR uses. Pinning MathComp 2.5.0 with analysis 1.16.0 and word 3.5, the same combination the flake CI uses, makes it green. The nix CI bundles pin similarly old versions and need the same update.
• Moving to analysis 1.17.0 on opam is blocked upstream: it needs MathComp 2.6.0, which the released extructures and mathcomp-word do not support yet. extructures needs a fix that is already on master, word mainly needs a tag. I cannot open issues on those repos.