proposition: Theorem SterbenzAux : forall x y : float, Fbounded b x -> Fbounded b y -> (y <= x)%R -> (x <= 2 * y)%R -> Fbounded b (Fminus radix x y).
proof: Proof. intros x y H' H'0 H'1 H'2. cut (0 <= Fminus radix x y)%R; [ intros Rle1 | idtac ]. cut (Fminus radix x y <= y)%R; [ intros Rle2 | idtac ]. case (Zle_or_lt (Fexp x) (Fexp y)); intros Zle1. repeat split. apply Z.le_lt_trans with (Z.abs (Fnum x)); try apply H'. change (Fnum (Fabs (Fminus radix x y)) <= Fnum (Fabs x))%Z in |- *. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. repeat rewrite Fabs_correct. repeat rewrite Rabs_pos_eq; auto. apply Rle_trans with (2 := H'1); auto. apply Rle_trans with (2 := H'1); auto. apply Rle_trans with (2 := Rle2); auto. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. unfold Fminus in |- *; simpl in |- *; apply Z.min_l; auto. unfold Fminus in |- *; simpl in |- *; rewrite Z.min_l; try easy. apply H'. repeat split. apply Z.le_lt_trans with (Z.abs (Fnum y)); try apply H'0. change (Fnum (Fabs (Fminus radix x y)) <= Fnum (Fabs y))%Z in |- *. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. repeat rewrite Fabs_correct. repeat rewrite Rabs_pos_eq; auto. apply Rle_trans with (2 := Rle2); auto. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. unfold Fminus in |- *; simpl in |- *; apply Z.min_r; auto with zarith. unfold Fminus in |- *; simpl in |- *; rewrite Z.min_r; try apply H'0; auto with zarith. rewrite (Fminus_correct radix); auto with arith; fold FtoRradix in |- *. apply Rplus_le_reg_l with (r := FtoRradix y); auto. replace (y + (x - y))%R with (FtoRradix x); [ idtac | ring ]. replace (y + y)%R with (2 * y)%R; [ auto | simpl in |- *; ring ]. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. rewrite (Fminus_correct radix); auto with arith; fold FtoRradix in |- *. apply Rplus_le_reg_l with (r := FtoRradix y); auto. replace (y + (x - y))%R with (FtoRradix x); [ idtac | ring ]. replace (y + 0)%R with (FtoRradix y); [ auto | simpl in |- *; ring ]. apply Z.lt_trans with (2 := radixMoreThanOne); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz