proposition: Theorem Sterbenz : forall x y : float, Fbounded b x -> Fbounded b y -> (/ 2 * 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 (y <= 2 * x)%R; [ intros Le1 | idtac ]. case (Rle_or_lt x y); intros Le2; auto. apply oppBoundedInv; auto. rewrite Fopp_Fminus. apply SterbenzAux; auto with real. apply SterbenzAux; auto with real. apply Rmult_le_reg_l with (r := (/ 2)%R). apply Rinv_0_lt_compat; auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. rewrite Rmult_1_l; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz