floor and ceil to be subsumed by MathComp #330
Description
TODO: revise the use of floor and ceil once math-comp/math-comp#682 is merged into MathComp requiring MC >= 2.1.0
{{ message }}
TODO: revise the use of floor and ceil once math-comp/math-comp#682 is merged into MathComp requiring MC >= 2.1.0