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; case: trunc_subproof => // n hn. by case: ifP => x_ge0; rewrite ?(ifT _ _ x_ge0) ?(ifF _ _ x_ge0) // hn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)