proposition: Fact ex7 : (forall x, F x -> F (-x)) -> round_pred_total (Rnd_DN_pt F) -> round_pred_total (Rnd_UP_pt F).
proof: Proof. intros sym tDN. intros x. destruct (tDN (-x)) as [y [Fy [yLx yM]]]. exists (-y); repeat split. - apply sym; auto. - lra. - intros g Fg xLg. assert (HH := yM _ (sym _ Fg)). lra. Qed.
imports: Psatz Reals Flocq(Core)