proposition: Lemma DN_UP_parity_aux : DN_UP_parity_pos_prop -> DN_UP_parity_prop.
proof: Proof. intros Hpos x xd xu Hfx Hd Hu Hxd Hxu. destruct (total_order_T 0 x) as [[Hx|Hx]|Hx]. exact (Hpos x xd xu Hx Hfx Hd Hu Hxd Hxu). elim Hfx. rewrite <- Hx. apply generic_format_0. assert (Hx': (0 < -x)%R). apply Ropp_lt_cancel. now rewrite Ropp_involutive, Ropp_0. destruct xd as (md, ed). destruct xu as (mu, eu). simpl. rewrite <- (Bool.negb_involutive (Z.even mu)). apply f_equal. apply sym_eq. rewrite <- (Z.even_opp mu), <- (Z.even_opp md). change (Z.even (Fnum (Float beta (-md) ed)) = negb (Z.even (Fnum (Float beta (-mu) eu)))). apply (Hpos (-x)%R _ _ Hx'). intros H. apply Hfx. rewrite <- Ropp_involutive. now apply generic_format_opp. now apply canonical_opp. now apply canonical_opp. rewrite round_DN_opp, F2R_Zopp. now apply f_equal. rewrite round_UP_opp, F2R_Zopp. now apply f_equal. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp