proposition: Lemma truncP x : if 0 <= x then (trunc x)%:R <= x < (trunc x).+1%:R else trunc x == 0%N.
proof: Proof. rewrite /trunc -numq_ge0; case: (ratP x) => -[] //= n d _. rewrite ler_pdivlMr ?ltr_pdivrMr ?ltr0z // -!natrM ler_nat ltr_nat. by rewrite leq_trunc_div ltn_ceil. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)