proposition: Lemma round_round_minus_aux0 : forall (fexp1 fexp2 : Z -> Z), round_round_plus_hyp fexp1 fexp2 -> forall x y, 0 < y -> y < x -> (fexp1 (mag x) - 1 <= mag y)%Z -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> generic_format beta fexp2 (x - y).
proof: Proof. intros fexp1 fexp2 Hexp x y Py Hyx Hln Fx Fy. assert (Px := Rlt_trans 0 y x Py Hyx). destruct Hexp as (Hexp1,(_,(Hexp3,Hexp4))). assert (Lyx : (mag y <= mag x)%Z); [now apply mag_le; [|apply Rlt_le]|]. destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - assert (Hor : (mag y = mag x :> Z) \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heq. apply Hexp4. apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. + apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heqm1. apply Hexp4. apply Zplus_le_compat_r. now apply mag_minus. - destruct (mag_minus_disj x y Px Py Hge) as [Lxmy|Lxmy]. + apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. lia. * now rewrite Lxmy; apply Hexp3. + apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; rewrite Lxmy. * apply Hexp1. replace (_ + _)%Z with (mag x : Z); [|ring]. now apply Z.le_trans with (mag y). * apply Hexp1. now replace (_ + _)%Z with (mag x : Z); [|ring]. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ