proposition: Lemma decreasing_in_Rmax_simpl : forall D f, decreasing_in D f -> forall x y, D x -> D y -> x <= y -> Rmax (f x) (f y) = f x.
proof: Proof. intros D f f_dec x y Dx Dy Hxy ; assert (flb_lt_fub : f y <= f x) by (apply f_dec ; assumption) ; unfold Rmax ; destruct (Rle_dec (f x) (f y)) ; intuition (auto with real). Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra