proposition: Lemma round_round_plus_radix_ge_3_aux0 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> round_round_plus_radix_ge_3_hyp fexp1 fexp2 -> forall x y, (0 < y)%R -> (y <= x)%R -> (fexp1 (mag x) <= 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 Hexp x y Py Hyx Hln Fx Fy. assert (Px := Rlt_le_trans 0 y x Py Hyx). assert (Nny : (0 <= y)%R); [now apply Rlt_le|]. destruct Hexp as (_,(Hexp2,(Hexp3,Hexp4))). destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt]. - assert (Lxy : mag (x + y) = mag x :> Z); [now apply (mag_plus_separated fexp1)|]. apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]; rewrite Lxy. + now apply Hexp4; lia. + now apply Hexp3; lia. - apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]. destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. + now apply Hexp4; lia. + apply Hexp2; apply (mag_le beta y x Py) in Hyx. replace (_ - _)%Z with (mag x : Z) by ring. lia. + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. * now apply Hexp3; lia. * apply Hexp2. replace (_ - _)%Z with (mag x : Z) by ring. lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ