proposition: Lemma trunc_def x n : n%:R <= x < n.+1%:R -> Def.trunc x = n.
proof: Proof. case/andP=> lemx ltxm1; apply/eqP; rewrite eqn_leq -ltnS -[(n <= _)%N]ltnS. have/trunc_itv/andP[lefx ltxf1]: 0 <= x by apply: le_trans lemx; apply: ler0n. by rewrite -!(ltr_nat R) 2?(@le_lt_trans _ _ x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)