proposition: Fact ex13 : forall x y f g, Rnd_N_pt F x f -> Rnd_N_pt F y g -> x < y -> f <= g.
proof: Proof. intros x y f g [Ff Pf] [Fg Pg] xLy. assert (Hg := Pf g Fg). assert (Hf := Pg f Ff). destruct (Rle_dec f g) as [fLg|fGg]; try lra. destruct (Rle_dec f x) as [fLx|fGx]. - rewrite !Rabs_left1 in Hg; try lra. rewrite !Rabs_left1 in Hf; try lra. - rewrite Rabs_right in Hg; try lra. destruct (Rle_dec g x) as [gLx|gGx]; try lra. rewrite Rabs_left1 in Hg; try lra. rewrite Rabs_left1 in Hf; try lra. destruct (Rle_dec f y) as [fLy|fGy]; try lra. rewrite Rabs_left1 in Hf; try lra. rewrite Rabs_right in Hf; try lra. rewrite Rabs_right in Hg; try lra. Qed.
imports: Psatz Reals Flocq(Core)