proposition: Lemma trunc_itv x : 0 <= x -> (Def.trunc x)%:R <= x < (Def.trunc x).+1%:R.
proof: Proof. by move=> x_ge0; move: (truncP x); rewrite x_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)