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