proposition: Fact ex14 : NG_existence_prop F Taway.
proof: Proof. intros x d u NFx DNd UPu. destruct (Rle_dec 0 x) as [xPos|xNPos]. - left; red. destruct (UPu) as [Fu [xLu _]]. rewrite !Rabs_right; lra. - right; red. destruct (DNd) as [Fd [dLx _]]. rewrite !Rabs_left1; lra. Qed.
imports: Psatz Reals Flocq(Core)