Library Coq.Reals.R_Ifp
Complements for the reals.Integer and fractional part
Require Import Rbase.
Require Import Omega.
Open Local Scope R_scope.
Lemma base_Int_part :
forall r:R,
IZR (
Int_part r) <=
r /\
IZR (
Int_part r) -
r > -1.
Lemma Int_part_INR :
forall n:nat,
Int_part (
INR n) =
Z_of_nat n.
Lemma fp_nat :
forall r:R,
frac_part r = 0 ->
exists c :
Z,
r =
IZR c.
Lemma R0_fp_O :
forall r:R, 0 <>
frac_part r -> 0 <>
r.
Lemma Rminus_Int_part1 :
forall r1 r2:R,
frac_part r1 >=
frac_part r2 ->
Int_part (
r1 -
r2) = (
Int_part r1 -
Int_part r2)%Z.
Lemma Rminus_Int_part2 :
forall r1 r2:R,
frac_part r1 <
frac_part r2 ->
Int_part (
r1 -
r2) = (
Int_part r1 -
Int_part r2 - 1)%Z.
Lemma Rminus_fp1 :
forall r1 r2:R,
frac_part r1 >=
frac_part r2 ->
frac_part (
r1 -
r2) =
frac_part r1 -
frac_part r2.
Lemma Rminus_fp2 :
forall r1 r2:R,
frac_part r1 <
frac_part r2 ->
frac_part (
r1 -
r2) =
frac_part r1 -
frac_part r2 + 1.
Lemma plus_Int_part1 :
forall r1 r2:R,
frac_part r1 +
frac_part r2 >= 1 ->
Int_part (
r1 +
r2) = (
Int_part r1 +
Int_part r2 + 1)%Z.
Lemma plus_Int_part2 :
forall r1 r2:R,
frac_part r1 +
frac_part r2 < 1 ->
Int_part (
r1 +
r2) = (
Int_part r1 +
Int_part r2)%Z.
Lemma plus_frac_part1 :
forall r1 r2:R,
frac_part r1 +
frac_part r2 >= 1 ->
frac_part (
r1 +
r2) =
frac_part r1 +
frac_part r2 - 1.
Lemma plus_frac_part2 :
forall r1 r2:R,
frac_part r1 +
frac_part r2 < 1 ->
frac_part (
r1 +
r2) =
frac_part r1 +
frac_part r2.