proposition: Theorem FshiftO : forall x : float, Fshift 0 x = x.
proof: Proof. intros x; unfold Fshift in |- *; apply floatEq; simpl in |- *. replace (Zpower_nat radix 0) with 1%Z; auto with zarith. simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz