proposition: Theorem sterbenz : forall x y, format x -> format y -> (y / 2 <= x <= 2 * y)%R -> format (x - y)%R.
proof: Proof. intros x y Hx Hy (Hxy1, Hxy2). destruct (Rle_or_lt x y) as [Hxy|Hxy]. rewrite <- Ropp_minus_distr. apply generic_format_opp. apply sterbenz_aux ; try easy. split. exact Hxy. apply Rcompare_not_Lt_inv. rewrite <- Rcompare_half_r. now apply Rcompare_not_Lt. apply sterbenz_aux ; try easy. split. now apply Rlt_le. exact Hxy2. Qed.
imports: Coq(ZArith Reals) Zaux Raux Defs Generic_fmt Operations