proposition: Lemma round_round_minus_aux1 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> round_round_plus_hyp fexp1 fexp2 -> forall x y, 0 < y -> y < x -> (mag y <= fexp1 (mag x) - 2)%Z -> (fexp1 (mag (x - y)) - 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 Vfexp1 Vfexp2 Hexp x y Py Hyx Hln Hln' Fx Fy. assert (Px := Rlt_trans 0 y x Py Hyx). destruct Hexp as (Hexp1,(Hexp2,(Hexp3,Hexp4))). assert (Lyx : (mag y <= mag x)%Z); [now apply mag_le; [|apply Rlt_le]|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - apply Z.le_trans with (fexp1 (mag (x - y))). + apply Hexp4; lia. + lia. - now apply Hexp3. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ