proposition: Lemma Int_part_ge0 a : 0 <= a -> (0 <= Int_part a)%Z.
proof: Proof. move/up_pos => ?; rewrite /Int_part (_ : 0 = Z.succ 0 - 1)%Z //. apply Z.sub_le_mono => //; exact/Zlt_le_succ. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)