proposition: Theorem Rnd_N_pt_monotone : forall F : R -> Prop, forall x y f g : R, Rnd_N_pt F x f -> Rnd_N_pt F y g -> x < y -> f <= g.
proof: Proof. intros F x y f g (Hf,Hx) (Hg,Hy) Hxy. apply Rnot_lt_le. intros Hgf. assert (Hfgx := Hx g Hg). assert (Hgfy := Hy f Hf). clear F Hf Hg Hx Hy. destruct (Rle_or_lt x g) as [Hxg|Hgx]. apply Rle_not_lt with (1 := Hfgx). rewrite 2!Rabs_pos_eq. now apply Rplus_lt_compat_r. apply Rle_0_minus. apply Rlt_le. now apply Rle_lt_trans with (1 := Hxg). now apply Rle_0_minus. assert (Hgy := Rlt_trans _ _ _ Hgx Hxy). destruct (Rle_or_lt f y) as [Hfy|Hyf]. apply Rle_not_lt with (1 := Hgfy). rewrite (Rabs_left (g - y)). 2: now apply Rlt_minus. rewrite Rabs_left1. apply Ropp_lt_contravar. now apply Rplus_lt_compat_r. now apply Rle_minus. rewrite Rabs_left, Rabs_pos_eq, Ropp_minus_distr in Hgfy. rewrite Rabs_pos_eq, Rabs_left, Ropp_minus_distr in Hfgx. apply Rle_not_lt with (1 := Rplus_le_compat _ _ _ _ Hfgx Hgfy). apply Rminus_lt. ring_simplify. apply Rlt_minus. apply Rmult_lt_compat_l. now apply IZR_lt. exact Hxy. now apply Rlt_minus. apply Rle_0_minus. apply Rlt_le. now apply Rlt_trans with (1 := Hxy). apply Rle_0_minus. now apply Rlt_le. now apply Rlt_minus. Qed.
imports: Coq(Reals) Raux Defs