proposition: Lemma frac_part_INR m : frac_part (INR m) = 0.
proof: Proof. rewrite /frac_part /Int_part -(up_tech _ (Z_of_nat m)). - by rewrite minus_IZR plus_IZR /= -INR_IZR_INZ; by field. - rewrite -INR_IZR_INZ. by apply/RleP; rewrite Order.POrderTheory.lexx. - rewrite {1}INR_IZR_INZ; apply IZR_lt. by apply Z.lt_add_pos_r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)