proposition: Theorem MSB_shift : forall (x : float) (n : nat), ~ is_Fzero x -> MSB x = MSB (Fshift radix n x).
proof: Proof. intros; unfold MSB, Fshift, Fdigit in |- *; simpl in |- *. rewrite digitAdd; try easy. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz