proposition: Lemma frac_Int_part x : frac_part x = 0 -> IZR (Int_part x) = x.
proof: Proof. rewrite /frac_part. set h := IZR _. move=> H. by rewrite -(addR0 h) -H Rplus_minus. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)