proposition: Fact trunc_subproof x : {m | 0 <= x -> m%:R <= x < m.+1%:R }.
proof: Proof. have [Rx | _] := boolP (0 <= x); last by exists 0%N. have/ex_minnP[n lt_x_n1 min_n]: exists n, x < n.+1%:R. by exists (bound x); rewrite (lt_trans (boundP Rx)) ?ltr_nat. exists n => _; rewrite {}lt_x_n1 andbT; case: n min_n => //= n min_n. rewrite real_leNgt ?rpred_nat ?ger0_real //; apply/negP => /min_n. by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)