proposition: Theorem round_plus_neq_0 : forall x y, format x -> format y -> (x + y <> 0)%R -> round beta fexp rnd (x + y) <> 0%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Hx Hy Hxy. destruct (Rle_or_lt 0 (x + y)) as [H1|H1]. destruct (Zle_or_lt (cexp beta fexp x) (cexp beta fexp y)) as [H2|H2]. apply round_plus_neq_0_aux... lra. rewrite Rplus_comm. apply round_plus_neq_0_aux ; try easy. now apply Zlt_le_weak. lra. rewrite <- (Ropp_involutive (x + y)), Ropp_plus_distr. rewrite round_opp. apply Ropp_neq_0_compat. destruct (Zle_or_lt (cexp beta fexp (-x)) (cexp beta fexp (-y))) as [H2|H2]. apply round_plus_neq_0_aux; try apply generic_format_opp... lra. rewrite Rplus_comm. apply round_plus_neq_0_aux; try apply generic_format_opp... now apply Zlt_le_weak. lra. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative