What is currently the best way to prove simple integrals in Coq? I guess it could be done in math-comp analysis and there seem to be some older libraries too. There are two unsolved problems on Freeks 100-list that i guess is boils down to simple integrals.

- The Area of a Circle ( http://www.cs.ru.nl/~freek/100/#9 )
- Buffon Needle Problem ( http://www.cs.ru.nl/~freek/100/#99 )

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (`coq-num-analysis`

package in Coq opam)

Karl Palmskog said:

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (

`coq-num-analysis`

package in Coq opam)

Nice. I'll have a look. (opam installation failed but that can probably be solved).

```
$ opam search coq-num-analysis
# Packages matching: match(*coq-num-analysis*)
# No matches found
```

you need to do `opam update`

, then `opam show coq-num-analysis.1.0.0`

works

and also make sure to add Coq opam `released`

repo as here: https://github.com/coq/opam-coq-archive#usage

Last updated: Jun 18 2024 at 10:02 UTC