proposition: Fact floor_subproof x : {m | if x \is Num.real then m%:~R <= x < (m + 1)%:~R else m == 0}.
proof: Proof. have [Rx | _] := boolP (x \is Num.real); last by exists 0. without loss x_ge0: x Rx / x >= 0. have [x_ge0 | /ltW x_le0] := real_ge0P Rx; first exact. case/(_ (- x)) => [||m]; rewrite ?rpredN ?oppr_ge0 //. rewrite lerNr ltrNl -!rmorphN opprD /= le_eqVlt. case: eqP => [-> _ | _ /andP[lt_x_m lt_m_x]]. by exists (- m); rewrite lexx rmorphD ltrDl ltr01. by exists (- m - 1); rewrite (ltW lt_m_x) subrK. by exists (Posz (trunc x)); rewrite addrC -intS -!pmulrn trunc_itv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)