proposition: Theorem MSB_comp : forall (x y : float) (n : nat), ~ is_Fzero x -> x = y :>R -> MSB x = MSB y.
proof: Proof. intros x y H' H'0 H'1. case (FshiftCorrectSym radix) with (2 := H'1); auto. intros m1 H'2; elim H'2; intros m2 E; clear H'2. rewrite (MSB_shift x m1); auto. rewrite E; auto. apply sym_equal; apply MSB_shift; auto. apply (NisFzeroComp radix) with (x := x); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz