proposition: Lemma trunc_floor x : trunc x = if 0 <= x then `|floor x|%N else 0%N.
proof: Proof. case: ifP => [x_ge0 | x_ge0F]; last first. by apply/trunc0Pn; apply/contraFN: x_ge0F; apply/le_trans. apply/trunc_def; rewrite !pmulrn intS addrC abszE; have/floor_le := x_ge0. by rewrite floor0 => /normr_idP ->; exact/floor_itv/ger0_real. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)