fact: Definition trunc_itv x : 0 <= x -> (trunc x)%:R <= x < (trunc x).+1%:R := @trunc_itv R x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)