fact: Definition truncP x : if 0 <= x then (trunc x)%:R <= x < (trunc x).+1%:R else trunc x == 0%N := Num.Internals.truncP x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)