proposition: Theorem MSBroundLSB : forall P : R -> float -> Prop, RoundedModeP b radix P -> forall f1 f2 : float, P f1 f2 -> ~ is_Fzero (Fminus radix f1 f2) -> (MSB radix (Fminus radix f1 f2) < LSB radix f2)%Z.
proof: Proof. intros P H' f1 f2 H'0 HZ. apply (oneExp_Zlt radix); auto. apply Rlt_le_trans with (Fulp b radix precision f2). apply Rle_lt_trans with (FtoRradix (Fabs (Fminus radix f1 f2))). unfold FtoRradix in |- *; apply MSB_le_abs; auto. unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith; rewrite Fminus_correct; auto with arith. apply RoundedModeUlp with (4 := H'); auto. apply FUlp_Le_LSigB; auto. apply RoundedModeBounded with (1 := H') (2 := H'0); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz