proposition: Lemma mag_plus_separated : forall fexp : Z -> Z, forall x y, 0 < x -> 0 <= y -> generic_format beta fexp x -> (mag y <= fexp (mag x))%Z -> (mag (x + y) = mag x :> Z).
proof: Proof. intros fexp x y Px Nny Fx Hsep. apply mag_plus_eps with (1 := Px) (2 := Fx). apply (conj Nny). rewrite <- Rabs_pos_eq with (1 := Nny). apply Rlt_le_trans with (1 := bpow_mag_gt beta _). rewrite ulp_neq_0 by now apply Rgt_not_eq. now apply bpow_le. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ