proposition: Lemma fp_R0 : frac_part 0 = 0.
proof: Proof. unfold frac_part, Int_part. replace (up 0) with 1%Z. - now rewrite <- minus_IZR. - destruct (archimed 0) as [H1 H2]. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. normZ. + slia H2 HZ. + slia H1 HZ. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac