proposition: Lemma round_plus_neq_0_aux : forall x y, (cexp beta fexp x <= cexp beta fexp y)%Z -> format x -> format y -> (0 < x + y)%R -> round beta fexp rnd (x + y) <> 0%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y He Hx Hy Hxy. destruct (mag beta (x + y)) as (exy, Hexy). simpl. specialize (Hexy (Rgt_not_eq _ _ Hxy)). destruct (Zle_or_lt exy (fexp exy)) as [He'|He']. assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) + Ztrunc (y * bpow (- fexp exy))) (fexp exy))). rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1. rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1. now rewrite <- F2R_plus, Fplus_same_exp. rewrite H. rewrite round_generic... rewrite <- H. now apply Rgt_not_eq. apply generic_format_F2R. intros _. rewrite <- H. unfold cexp. rewrite mag_unique with (1 := Hexy). apply Z.le_refl. intros H. elim Rle_not_lt with (1 := round_le beta _ rnd _ _ (proj1 Hexy)). rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hxy)). rewrite H. rewrite round_generic... apply bpow_gt_0. apply generic_format_bpow. apply Zlt_succ_le. now rewrite (Zsucc_pred exy) in He'. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative