proposition: Lemma sterbenz_aux : forall x y, format x -> format y -> (y <= x <= 2 * y)%R -> format (x - y)%R.
proof: Proof. intros x y Hx Hy (Hxy1, Hxy2). unfold Rminus. apply generic_format_plus_weak. exact Hx. now apply generic_format_opp. rewrite Rabs_pos_eq. rewrite Rabs_Ropp. rewrite Rmin_comm. assert (Hy0: (0 <= y)%R). apply Rplus_le_reg_r with y. apply Rle_trans with x. now rewrite Rplus_0_l. now replace (y + y)%R with (2 * y)%R by ring. rewrite Rabs_pos_eq with (1 := Hy0). rewrite Rabs_pos_eq. unfold Rmin. destruct (Rle_dec y x) as [Hyx|Hyx]. apply Rplus_le_reg_r with y. now ring_simplify. now elim Hyx. now apply Rle_trans with y. now apply Rle_0_minus. Qed.
imports: Coq(ZArith Reals) Zaux Raux Defs Generic_fmt Operations