proposition: Fact ex15 x y : Monotone_exp phi -> generic_format r phi x -> generic_format r phi y -> (y / 2 <= x <= 2 * y)%R -> generic_format r phi (x - y)%R.
proof: Proof. intros mPhi Hx Hy (Hxy1, Hxy2). destruct (Req_dec (x - y) 0) as [xEy | xNEy]. rewrite xEy; apply generic_format_0. unfold generic_format, cexp in Hx, Hy. assert (Hx1 := bpow_mag_gt r x). rewrite Rabs_right in Hx1; try lra. set (ex := (mag r x) : Z) in *. set (mx := Ztrunc (_ _ x)) in *. set (fx := {| Fnum := mx; Fexp := _ |}) in *. assert (Hy1 := bpow_mag_gt r y). rewrite Rabs_right in Hy1; try lra. set (ey := (mag r y) : Z) in *. set (my := Ztrunc (_ _ y)) in *. set (fy := {| Fnum := my; Fexp := _ |}) in *. rewrite Hx, Hy, <- F2R_minus. assert (Fm := F2R_minus fx fy). rewrite <-Hx, <-Hy in Fm. assert (Hxy : Fexp (Fminus fx fy) = Z.min (phi ex) (phi ey)). apply Fexp_Fplus. destruct (Fminus fx fy) as [mxy exy]. apply generic_format_F2R; simpl. intros _. rewrite Fm; simpl in Hxy. unfold cexp. rewrite Hxy. destruct (Zmin_spec (phi ex) (phi ey)) as [(H1,H2)|(H1,H2)]; rewrite H2; apply mPhi; apply mag_le_abs; try lra; split_Rabs; lra. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)