search

coq-community / apery

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
Other
19 stars 6 forks source link

Clean up extra_*.v material #7

Open amahboubi opened 2 years ago

amahboubi commented 2 years ago

Tidy the missing-at-the-time-of-writing material: a few petty lemmas plus some results on Cauchy reals.

pi8027 commented 4 months ago

FTR, floorQ in floor.v should now be replaced by Num.floor (defined in archimedean.v for any archiNumDomainType).

pi8027 commented 3 months ago

FTR, floorQ in floor.v should now be replaced by Num.floor (defined in archimedean.v for any archiNumDomainType).

Done in #24.