proposition: Lemma truncP x : if 0 <= x then (Def.trunc x)%:R <= x < (Def.trunc x).+1%:R else Def.trunc x == 0%N.
proof: Proof. exact: trunc_subproof. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)