affeldt-aist

I tried again today with Alectryon 1.4.0, coq-serapi 8.15.0+0.15.0, coq 8.15.2 and it seems that it could generate html versions for all files, see https://math-comp.github.io/analysis/htmldoc_master_alectryon/. However there were a number...

>

> Do you want them removed completely, or dynamically shown/hidden with a click? Dynamic would be great but we were only thinking about hiding as with coqdoc. In fact, so...

Maybe this could help: https://www.isa-afp.org/entries/Eudoxus_Reals.html

I think that we'd like to use `wochoice.v` in `classical_sets.v` but the simple fact of `Require Import`ing `wochoice` in `classical_sets.v` leads to: ```coq File "./theories/derive.v", line 5, characters 0-79: Error:...

@proux01 @CohenCyril any quick hint? (We are in the process of deriving our Zorn's lemmas from Georges'.)

@proux01 Thank you for the pointer! (I didn't know.) I was able to avoid the universe inconsistency without really understanding it by just removing useless `Require Import`'s, which means that...

We tried a tentative fix for the definition of `C1`. We can mostly patch the lemma `C1_lipschitz`. The only remaining problem is to show: ``` dfa : derivable_right f a...

resolved by #923

@hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the `Section cvg_random_variable`.