proposition: Lemma round_round_plus_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 Hlnx Hlny Fx Fy. destruct (Z.le_gt_cases (fexp1 (mag x)) (fexp1 (mag y))) as [Hle|Hgt]. - now apply (round_round_plus_aux0_aux_aux fexp1). - rewrite Rplus_comm in Hlnx, Hlny |- *. now apply (round_round_plus_aux0_aux_aux fexp1); [lia| | | |]. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ