proposition: Fact ex15 : F 0 -> Rnd_NG_pt_unique_prop F Taway.
proof: Proof. intros F0 x d u [Fd [dLx Pd]] [_ Nd] [Fu [xLu Pu]] [_ Nu]. unfold Taway. destruct (Rle_dec 0 x) as [xPos|xNPos]. - rewrite (Rabs_right x); try lra. assert (dPos : 0 <= d). apply Pd; try lra; auto. rewrite Rabs_right; try lra. intros dGx _. assert (xEd : x = d); try lra. assert (HH := Nu d Fd). rewrite !Rabs_right in HH; lra. - rewrite (Rabs_left1 x); try lra. assert (uNeg : u <= 0). apply Pu; try lra; auto. rewrite (Rabs_left1 u); try lra. intros _ uLx. assert (xEu : x = u); try lra. assert (HH := Nd u Fu). rewrite !Rabs_left1 in HH; lra. Qed.
imports: Psatz Reals Flocq(Core)