proposition: Theorem FshiftCorrect : forall (n : nat) (x : float), Fshift n x = x :>R.
proof: Proof. intros n x; unfold FtoR in |- *; simpl in |- *. rewrite mult_IZR. rewrite Zpower_nat_Z_powerRZ; auto. repeat rewrite Rmult_assoc. rewrite <- powerRZ_add. rewrite Zplus_minus; auto. now apply Rgt_not_eq, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz