Clean up extra_*.v material

[amahboubi]

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

[pi8027]

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

[pi8027]

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

Done in #24.