proposition: Lemma round_round_minus_aux0_aux : forall (fexp1 fexp2 : Z -> Z), forall x y, (fexp2 (mag (x - y))%Z <= fexp1 (mag x))%Z -> (fexp2 (mag (x - y))%Z <= fexp1 (mag y))%Z -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> generic_format beta fexp2 (x - y).
proof: Proof. intros fexp1 fexp2 x y. replace (x - y)%R with (x + (- y))%R; [|ring]. intros Hlnx Hlny Fx Fy. rewrite <- (mag_opp beta y) in Hlny. apply generic_format_opp in Fy. now apply (round_round_plus_aux0_aux fexp1). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ