proposition: Theorem FshiftFdigit : forall (n : nat) (x : float), ~ is_Fzero x -> Fdigit (Fshift n x) = Fdigit x + n.
proof: Proof. intros n x; case x; unfold Fshift, Fdigit, is_Fzero in |- *; simpl in |- *. intros p1 p2 H; apply digitAdd; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz