proposition: Theorem LSB_shift : forall (x : float) (n : nat), ~ is_Fzero x -> LSB x = LSB (Fshift radix n x).
proof: Proof. intros x n H'; unfold LSB, Fdigit in |- *; simpl in |- *. rewrite digitAdd; auto with arith. rewrite maxDivPlus; auto. rewrite inj_plus; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz