proposition: Lemma fp_nat : forall r:R, frac_part r = 0 -> exists c : Z, r = IZR c.
proof: Proof. unfold frac_part; intros; split with (Int_part r); apply Rminus_diag_uniq; auto with zarith real. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac