diff --git a/.github/workflows/nix-action-8.16.yml b/.github/workflows/nix-action-8.16.yml
deleted file mode 100644
index 994c1fa6e..000000000
--- a/.github/workflows/nix-action-8.16.yml
+++ /dev/null
@@ -1,283 +0,0 @@
-jobs:
-  coq:
-    needs: []
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target coq
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.16\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "coq"
-  mathcomp:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.16\" --argstr job \"mathcomp\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-ssreflect"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-fingroup'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-fingroup"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-algebra'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-algebra"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-solvable'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-solvable"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-character'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-character"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp"
-  mathcomp-analysis:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.16\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2>&1\
-        \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
-        built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-classical'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-classical"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-bigenough'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-bigenough"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-analysis"
-  mathcomp-analysis-single:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis-single
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.16\" --argstr job \"mathcomp-analysis-single\" \\\n   --dry-run\
-        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
-        \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-algebra'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-algebra"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-finmap'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-finmap"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-bigenough'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-bigenough"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr
-        job "mathcomp-analysis-single"
-name: Nix CI for bundle 8.16
-'on':
-  pull_request:
-    paths:
-    - .github/workflows/nix-action-8.16.yml
-  pull_request_target:
-    paths-ignore:
-    - .github/workflows/nix-action-8.16.yml
-    types:
-    - opened
-    - synchronize
-    - reopened
-  push:
-    branches:
-    - master
diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml
deleted file mode 100644
index 0a5a0f806..000000000
--- a/.github/workflows/nix-action-8.17.yml
+++ /dev/null
@@ -1,283 +0,0 @@
-jobs:
-  coq:
-    needs: []
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target coq
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.17\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "coq"
-  mathcomp:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.17\" --argstr job \"mathcomp\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-ssreflect"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-fingroup'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-fingroup"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-algebra'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-algebra"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-solvable'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-solvable"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-character'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-character"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp"
-  mathcomp-analysis:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.17\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2>&1\
-        \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
-        built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-classical'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-classical"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-bigenough'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-bigenough"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-analysis"
-  mathcomp-analysis-single:
-    needs:
-    - coq
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
-        \ }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
-        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
-        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
-        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
-        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
-        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
-        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
-        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v3
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v20
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis-single
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"8.17\" --argstr job \"mathcomp-analysis-single\" \\\n   --dry-run\
-        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
-        \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-algebra'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-algebra"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-finmap'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-finmap"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-field'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-field"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-bigenough'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-bigenough"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: hierarchy-builder'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "hierarchy-builder"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr
-        job "mathcomp-analysis-single"
-name: Nix CI for bundle 8.17
-'on':
-  pull_request:
-    paths:
-    - .github/workflows/nix-action-8.17.yml
-  pull_request_target:
-    paths-ignore:
-    - .github/workflows/nix-action-8.17.yml
-    types:
-    - opened
-    - synchronize
-    - reopened
-  push:
-    branches:
-    - master
diff --git a/.nix/config.nix b/.nix/config.nix
index 5a19a6fda..89ae78de8 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -31,23 +31,15 @@
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "8.18";
+  default-bundle = "8.19";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles."8.16".coqPackages = {
-    coq.override.version = "8.16";
-    mathcomp.override.version = "2.0.0";
-  };
-  bundles."8.17".coqPackages = {
-    coq.override.version = "8.17";
-    mathcomp.override.version = "2.1.0";
-  };
   bundles."8.18".coqPackages = {
     coq.override.version = "8.18";
-    mathcomp.override.version = "2.2.0";
+    mathcomp.override.version = "2.1.0";
   };
 
   bundles."8.19".coqPackages = {
diff --git a/INSTALL.md b/INSTALL.md
index 157096836..fa0f98e2b 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -2,8 +2,8 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.16](https://coq.inria.fr)
-- [Mathematical Components version ≥ 2.0.0](https://github.com/math-comp/math-comp)
+- [The Coq Proof Assistant version ≥ 8.18](https://coq.inria.fr)
+- [Mathematical Components version ≥ 2.1.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.0.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.4.0](https://github.com/math-comp/hierarchy-builder)
 - [bigenough >= 1.0.0](https://github.com/math-comp/bigenough)
@@ -71,7 +71,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.18.0 and MathComp 2.0.0. For other versions, update the
+With the example of Coq 8.18.0 and MathComp 2.1.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.18.0
@@ -80,11 +80,11 @@ $ opam install coq.8.18.0
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.0.0
-$ opam install coq-mathcomp-fingroup.2.0.0
-$ opam install coq-mathcomp-algebra.2.0.0
-$ opam install coq-mathcomp-solvable.2.0.0
-$ opam install coq-mathcomp-field.2.0.0
+$ opam install coq-mathcomp-ssreflect.2.1.0
+$ opam install coq-mathcomp-fingroup.2.1.0
+$ opam install coq-mathcomp-algebra.2.1.0
+$ opam install coq-mathcomp-solvable.2.1.0
+$ opam install coq-mathcomp-field.2.1.0
 ```
 3. Install the Finite maps library
 ```
diff --git a/README.md b/README.md
index ee21b4ce3..7b5f14dae 100644
--- a/README.md
+++ b/README.md
@@ -34,13 +34,13 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.16 to 8.19 (or dev)
+- Compatible Coq versions: Coq 8.18 to 8.19 (or dev)
 - Additional dependencies:
-  - [MathComp ssreflect 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp fingroup 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp solvable 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp field 2.0.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp solvable 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.1.0 or later](https://math-comp.github.io)
   - [MathComp finmap 2.0.0](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
   - [Hierarchy Builder 1.4.0 or later](https://github.com/math-comp/hierarchy-builder)
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 019a74d23..98dee74c5 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -27,255 +27,6 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-(**************************)
-(* MathComp 2.1 additions *)
-(**************************)
-
-From mathcomp Require Import poly.
-
-Definition coefE :=
-  (coef0, coef1, coefC, coefX, coefXn,
-   coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
-   coefN, coefB, coefD,
-   coef_cons, coef_Poly, coef_poly,
-   coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
-   coef_comp_poly).
-
-Module Export Pdeg2.
-
-Module Export Field.
-
-Section Pdeg2Field.
-Variable F : fieldType.
-Hypothesis nz2 : 2%:R != 0 :> F.
-
-Variable p : {poly F}.
-Hypothesis degp : size p = 3%N.
-
-Let a := p`_2.
-Let b := p`_1.
-Let c := p`_0.
-
-Let pneq0 : p != 0. Proof. by rewrite -size_poly_gt0 degp. Qed.
-Let aneq0 : a != 0.
-Proof. by move: pneq0; rewrite -lead_coef_eq0 lead_coefE degp. Qed.
-Let a2neq0 : 2%:R * a != 0. Proof. by rewrite mulf_neq0. Qed.
-Let sqa2neq0 : (2%:R * a) ^+ 2 != 0. Proof. exact: expf_neq0. Qed.
-
-Let aa4 : 4%:R * a * a = (2%:R * a)^+2.
-Proof. by rewrite expr2 mulrACA mulrA -natrM. Qed.
-
-Let splitr (x : F) : x = x / 2%:R + x / 2%:R.
-Proof.
-apply: (mulIf nz2); rewrite -mulrDl mulfVK//.
-by rewrite -[2%:R]/(1 + 1)%:R natrD mulrDr mulr1.
-Qed.
-
-Let pE : p = a *: 'X^2 + b *: 'X + c%:P.
-Proof.
-apply/polyP => + /[!coefE] => -[|[|[|i]]] /=; rewrite !Monoid.simpm//.
-by rewrite nth_default// degp.
-Qed.
-
-Let delta := b ^+ 2 - 4%:R * a * c.
-
-Lemma deg2_poly_canonical :
-  p = a *: (('X + (b / (2%:R * a))%:P)^+2 - (delta / (4%:R * a ^+ 2))%:P).
-Proof.
-rewrite pE sqrrD -!addrA scalerDr; congr +%R; rewrite addrA scalerDr; congr +%R.
-- rewrite -mulrDr -polyCD -!mul_polyC mulrA mulrAC -polyCM.
-  by rewrite [a * _]mulrC mulrDl invfM -!mulrA mulVf// mulr1 -splitr.
-- rewrite [a ^+ 2]expr2 mulrA aa4 -polyC_exp -polyCB expr_div_n -mulrBl subKr.
-  by rewrite -mul_polyC -polyCM mulrCA mulrACA aa4 mulrCA mulfV// mulr1.
-Qed.
-
-Variable r : F.
-Hypothesis r_sqrt_delta : r ^+ 2 = delta.
-
-Let r1 := (- b - r) / (2%:R * a).
-Let r2 := (- b + r) / (2%:R * a).
-
-Lemma deg2_poly_factor : p = a *: ('X - r1%:P) * ('X - r2%:P).
-Proof.
-rewrite [p]deg2_poly_canonical//= -/a -/b -/c -/delta /r1 /r2.
-rewrite ![(- b + _) * _]mulrDl 2!polyCD 2!opprD 2!addrA !mulNr !polyCN !opprK.
-rewrite -scalerAl [in RHS]mulrC -subr_sqr -polyC_exp -[4%:R]/(2 * 2)%:R natrM.
-by rewrite -expr2 -exprMn [in RHS]exprMn exprVn r_sqrt_delta.
-Qed.
-
-End Pdeg2Field.
-End Field.
-
-Module Real.
-
-Section Pdeg2Real.
-
-Variable F : realFieldType.
-
-Section Pdeg2RealConvex.
-
-Variable p : {poly F}.
-Hypothesis degp : size p = 3%N.
-
-Let a := p`_2.
-Let b := p`_1.
-Let c := p`_0.
-
-Hypothesis age0 : 0 <= a.
-
-Let delta := b ^+ 2 - 4%:R * a * c.
-
-Let pneq0 : p != 0. Proof. by rewrite -size_poly_gt0 degp. Qed.
-Let aneq0 : a != 0.
-Proof. by move: pneq0; rewrite -lead_coef_eq0 lead_coefE degp. Qed.
-Let agt0 : 0 < a. Proof. by rewrite lt_def aneq0. Qed.
-Let a4gt0 : 0 < 4%:R * a. Proof. by rewrite mulr_gt0 ?ltr0n. Qed.
-
-Lemma deg2_poly_min x : p.[- b / (2%:R * a)] <= p.[x].
-Proof.
-rewrite [p]deg2_poly_canonical ?pnatr_eq0// -/a -/b -/c /delta !hornerE/=.
-by rewrite ler_pM2l// lerD2r addrC mulNr subrr ?mulr0 ?expr0n sqr_ge0.
-Qed.
-
-Lemma deg2_poly_minE : p.[- b / (2%:R * a)] = - delta / (4%:R * a).
-Proof.
-rewrite [p]deg2_poly_canonical ?pnatr_eq0// -/a -/b -/c -/delta !hornerE/=.
-rewrite -?expr2 [X in X^+2]addrC [in LHS]mulNr subrr expr0n add0r mulNr.
-by rewrite mulrC mulNr invfM mulrA mulfVK.
-Qed.
-
-Lemma deg2_poly_ge0 : reflect (forall x, 0 <= p.[x]) (delta <= 0).
-Proof.
-apply/(iffP idP) => [dlt0 x | /(_ (- b / (2%:R * a)))]; last first.
-  by rewrite deg2_poly_minE ler_pdivlMr// mul0r oppr_ge0.
-apply: le_trans (deg2_poly_min _).
-by rewrite deg2_poly_minE ler_pdivlMr// mul0r oppr_ge0.
-Qed.
-
-End Pdeg2RealConvex.
-
-End Pdeg2Real.
-
-Section Pdeg2RealClosed.
-
-Variable F : rcfType.
-
-Section Pdeg2RealClosedConvex.
-
-Variable p : {poly F}.
-Hypothesis degp : size p = 3%N.
-
-Let a := p`_2.
-Let b := p`_1.
-Let c := p`_0.
-
-Let nz2 : 2%:R != 0 :> F. Proof. by rewrite pnatr_eq0. Qed.
-
-Let delta := b ^+ 2 - 4%:R * a * c.
-
-Let r1 := (- b - Num.sqrt delta) / (2%:R * a).
-Let r2 := (- b + Num.sqrt delta) / (2%:R * a).
-
-Lemma deg2_poly_factor : 0 <= delta -> p = a *: ('X - r1%:P) * ('X - r2%:P).
-Proof. by move=> dge0; apply: deg2_poly_factor; rewrite ?sqr_sqrtr. Qed.
-
-End Pdeg2RealClosedConvex.
-
-End Pdeg2RealClosed.
-End Real.
-
-End Pdeg2.
-
-Section Degle2PolyRealConvex.
-
-Variable (F : realFieldType) (p : {poly F}).
-Hypothesis degp : (size p <= 3)%N.
-
-Let a := p`_2.
-Let b := p`_1.
-Let c := p`_0.
-
-Let delta := b ^+ 2 - 4%:R * a * c.
-
-Lemma deg_le2_poly_delta_ge0 : 0 <= a -> (forall x, 0 <= p.[x]) -> delta <= 0.
-Proof.
-move=> age0 pge0; move: degp; rewrite leq_eqVlt => /orP[/eqP|] degp'.
-  exact/(Real.deg2_poly_ge0 degp' age0).
-have a0 : a = 0 by rewrite /a nth_default.
-rewrite /delta a0 mulr0 mul0r subr0 exprn_even_le0//=.
-have [//|/eqP nzb] := eqP; move: (pge0 ((- 1 - c) / b)).
-have -> : p = b *: 'X + c%:P.
-  apply/polyP => + /[!coefE] => -[|[|i]] /=; rewrite !Monoid.simpm//.
-  by rewrite nth_default// -ltnS (leq_trans degp').
-by rewrite !hornerE/= mulrAC mulfV// mul1r subrK ler0N1.
-Qed.
-
-End Degle2PolyRealConvex.
-
-Section Degle2PolyRealClosedConvex.
-
-Variable (F : rcfType) (p : {poly F}).
-Hypothesis degp : (size p <= 3)%N.
-
-Let a := p`_2.
-Let b := p`_1.
-Let c := p`_0.
-
-Let delta := b ^+ 2 - 4%:R * a * c.
-
-Lemma deg_le2_poly_ge0 : (forall x, 0 <= p.[x]) -> delta <= 0.
-Proof.
-have [age0|alt0] := leP 0 a; first exact: deg_le2_poly_delta_ge0.
-move=> pge0; move: degp; rewrite leq_eqVlt => /orP[/eqP|] degp'; last first.
-  by move: alt0; rewrite /a nth_default ?ltxx.
-have [//|dge0] := leP delta 0.
-pose r1 := (- b - Num.sqrt delta) / (2%:R * a).
-pose r2 := (- b + Num.sqrt delta) / (2%:R * a).
-pose x0 := Num.max (r1 + 1) (r2 + 1).
-move: (pge0 x0); rewrite (Real.deg2_poly_factor degp' (ltW dge0)).
-rewrite !hornerE/= -mulrA nmulr_rge0// leNgt => /negbTE<-.
-by apply: mulr_gt0; rewrite subr_gt0 lt_maxr ltrDl ltr01 ?orbT.
-Qed.
-
-End Degle2PolyRealClosedConvex.
-
-Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.
-Proof. by rewrite GRing.mulrSr. Qed.
-
-Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.
-Proof. by rewrite GRing.mulrS. Qed.
-
-(* NB: became an equality in MC *)
-Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
-Proof. by move=> y0; rewrite lerBlDl lerDr. Qed.
-
-Section normr.
-Variable R : realDomainType.
-
-Definition Rnpos : qualifier 0 R := [qualify x : R | x <= 0].
-Lemma nposrE x : (x \is Rnpos) = (x <= 0). Proof. by []. Qed.
-
-Lemma ger0_le_norm :
-  {in Num.nneg &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
-Proof. by move=> x y; rewrite !nnegrE => x0 y0; rewrite !ger0_norm. Qed.
-
-Lemma gtr0_le_norm :
-  {in Num.pos &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
-Proof. by move=> x y; rewrite !posrE => /ltW x0 /ltW y0; exact: ger0_le_norm. Qed.
-
-Lemma ler0_ge_norm :
-  {in Rnpos &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
-Proof.
-move=> x y; rewrite !nposrE => x0 y0.
-by rewrite !ler0_norm// -subr_ge0 opprK addrC subr_ge0.
-Qed.
-
-Lemma ltr0_ge_norm :
-  {in Num.neg &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
-Proof. by move=> x y; rewrite !negrE => /ltW x0 /ltW y0; exact: ler0_ge_norm. Qed.
-
-End normr.
-
 (**************************)
 (* MathComp 2.2 additions *)
 (**************************)
@@ -346,6 +97,8 @@ Arguments dfwith {I T} f i x.
 (* not yet backported *)
 (**********************)
 
+From mathcomp Require Import poly.
+
 Lemma deg_le2_ge0 (F : rcfType) (a b c : F) :
   (forall x, 0 <= a * x ^+ 2 + b * x + c)%R -> (b ^+ 2 - 4%:R * a * c <= 0)%R.
 Proof.
diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam
index dc3e54ccf..ec55f13a3 100644
--- a/coq-mathcomp-classical.opam
+++ b/coq-mathcomp-classical.opam
@@ -18,8 +18,8 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.16" & < "8.20~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.0.0") | (= "dev") }
+  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.1.0") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
   "coq-mathcomp-finmap" { (>= "2.0.0") | (= "dev") }
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 3d08c035c..13cc2fdc3 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -290,7 +290,7 @@ Section ERealZsemimodule.
 Context {R : nmodType}.
 Implicit Types x y z : \bar R.
 
-Definition adde_subdef x y :=
+Definition adde x y :=
   match x, y with
   | x%:E , y%:E  => (x + y)%:E
   | -oo, _     => -oo
@@ -298,10 +298,9 @@ Definition adde_subdef x y :=
   | +oo, _     => +oo
   | _    , +oo => +oo
   end.
+Arguments adde : simpl never.
 
-Definition adde := nosimpl adde_subdef.
-
-Definition dual_adde_subdef x y :=
+Definition dual_adde x y :=
   match x, y with
   | x%:E , y%:E  => (x + y)%R%:E
   | +oo, _     => +oo
@@ -309,8 +308,7 @@ Definition dual_adde_subdef x y :=
   | -oo, _     => -oo
   | _    , -oo => -oo
   end.
-
-Definition dual_adde := nosimpl dual_adde_subdef.
+Arguments dual_adde : simpl never.
 
 Lemma addeA_subproof : associative (S := \bar R) adde.
 Proof. by case=> [x||] [y||] [z||] //; rewrite /adde /= addrA. Qed.
@@ -342,6 +340,8 @@ Definition enatmul x n : \bar R := iterop n +%R x 0.
 Definition ednatmul (x : \bar^d R) n : \bar^d R := iterop n +%R x 0.
 
 End ERealZsemimodule.
+Arguments adde : simpl never.
+Arguments dual_adde : simpl never.
 
 Section ERealOrder_numDomainType.
 Context {R : numDomainType}.
@@ -459,20 +459,20 @@ Section ERealArith.
 Context {R : numDomainType}.
 Implicit Types x y z : \bar R.
 
-Definition mule_subdef x y :=
+Definition mule x y :=
   match x, y with
   | x%:E , y%:E => (x * y)%:E
   | -oo, y | y, -oo => if y == 0 then 0 else if 0 < y then -oo else +oo
   | +oo, y | y, +oo => if y == 0 then 0 else if 0 < y then +oo else -oo
   end.
-
-Definition mule := nosimpl mule_subdef.
+Arguments mule : simpl never.
 
 Definition abse x : \bar R := if x is r%:E then `|r|%:E else +oo.
 
 Definition expe x n := iterop n mule x 1.
 
 End ERealArith.
+Arguments mule : simpl never.
 
 Notation "+%dE"  := (@GRing.add (\bar^d _)).
 Notation "+%E"   := (@GRing.add (\bar _)).
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 9c7242154..3b7e455c4 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2928,10 +2928,10 @@ move=> [s||]/=.
     by apply/nbhs_EFin; near do rewrite fin_numM//.
   move=> P /= Prs; apply/nbhs_EFin=> //=.
   by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst.
-- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
+- 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_pdivr_mull.
-- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
+- rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
   by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull.
 Unshelve. all: by end_near. Qed.
diff --git a/theories/topology.v b/theories/topology.v
index 61e4e257c..645ef864c 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -765,7 +765,7 @@ Class ProperFilter' {T : Type} (F : set_system T) := {
   filter_filter' : Filter F
 }.
 (* TODO: Reuse :> above and remove the following line and the coercion below
-   after 8.17 is the minimum required version for Coq *)
+   after 8.21 is the minimum required version for Coq *)
 Global Existing Instance filter_filter'.
 Global Hint Mode ProperFilter' - ! : typeclass_instances.
 Arguments filter_not_empty {T} F {_}.
@@ -3031,12 +3031,9 @@ Unshelve. all: by end_near. Qed.
 Section UltraFilters.
 
 Class UltraFilter T (F : set_system T) := {
-  ultra_proper : ProperFilter F ;
+  #[global] ultra_proper :: ProperFilter F ;
   max_filter : forall G : set_system T, ProperFilter G -> F `<=` G -> G = F
 }.
-(* When requiring Coq >= 8.17, replace the line below with
-  #[global] ultra_proper :: ProperFilter F ; *)
-#[global] Existing Instance ultra_proper.
 
 Lemma ultra_cvg_clusterE (T : topologicalType) (F : set_system T) :
   UltraFilter F -> cluster F = [set p | F --> p].